| 基于时间Ambient演算的业务流程模型验证 |
| |
| 引用本文： | 李津,李勇,高春呜.基于时间Ambient演算的业务流程模型验证[J].计算机工程与设计,2008,29(3):554-559. |
| |
| 作者姓名： | 李津 李勇 高春呜 |
| |
| 作者单位： | 1. 湖南师范大学,数学与计算机科学学院,湖南,长沙,410081
2. 湖南师范大学,数学与计算机科学学院,湖南,长沙,410081;国防科技大学,计算机学院,湖南,长沙,410073 |
| |
| 基金项目： | 湖南省科技攻关项目
,
湖南省自然科学基金
,
长沙市科技攻关重大基金 |
| |
| 摘 要： | Mobile Ambient演算是一种描述进程和设备移动的形式化方法,但其移动进程的实时性目前尚未有合适的形式化表达.通过对Mobile Ambient演算进行实时扩充,提出了一种离散时间域的时间Mobile Ambient演算(DTMA),并为DTMA演算定义了模态逻辑.基于DTMA演算及其模态逻辑的子集给出了模型验证算法,提出了一种对BPEL4WS程序的形式化建模方法,实现了业务流程的活动可达性的模型验证.
|
| 关 键 词： | 离散时间Ambient演算 移动进程 模态逻辑 模型验证 业务流程执行语言 |
| 文章编号： | 1000-7024（2008）03-0554-06 |
| 收稿时间： | 2007-03-16 |
| 修稿时间： | 2007年3月16日 |
Model checking for BPEL4WS based on timed Ambient |
| |
| LI Jin,LI Yong,GAO Chun-ming.Model checking for BPEL4WS based on timed Ambient[J].Computer Engineering and Design,2008,29(3):554-559. |
| |
| Authors: | LI Jin LI Yong GAO Chun-ming |
| |
| Abstract: | The Mobile Ambient calculus presented by Luca Cardelli is a formalism for describing the mobility of both process and mobile device, but the real-time property of the mobility has not been well described. Discrete time Mobile Ambient calculus (DTMA) is presented, which is extended by Mobile Ambient calculus with time. Based on a subset of the modal logic for DTMA, a model checking algorithm for DTMA is proposed. Finally an approach for modeling BPEL4WS is presented and by this method the model checking for reachability of the action in business process is implemented. |
| |
| Keywords: | discrete timed mobile Ambient mobile agent modal logic model checking BPEL4WS |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
