基于时间Ambient演算的业务流程模型验证  

Model checking for BPEL4WS based on timed Ambient

作　　者：李津[1] 李勇[1] 高春鸣[1] 

机构地区：[1]湖南师范大学数学与计算机科学学院,湖南长沙410081

出　　处：《计算机工程与设计》2008年第3期554-559,共6页Computer Engineering and Design

基　　金：湖南省重点科技攻关基金项目(05GK2002);湖南省自然科学基金项目(03JJY6023);长沙市科技攻关重大基金项目(K06070001-12)

摘　　要：Mobile Ambient演算是一种描述进程和设备移动的形式化方法,但其移动进程的实时性目前尚未有合适的形式化表达。通过对Mobile Ambient演算进行实时扩充,提出了一种离散时间域的时间Mobile Ambient演算(DTMA),并为DTMA演算定义了模态逻辑。基于DTMA演算及其模态逻辑的子集给出了模型验证算法,提出了一种对BPEL4WS程序的形式化建模方法,实现了业务流程的活动可达性的模型验证。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 BPEIAWS is presented and by this method the model checking for teachability of the action in business process is implemented.

关 键 词：离散时间Ambient演算 移动进程 模态逻辑 模型验证 业务流程执行语言 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]