支持业务事务验证的服务协调模型  

Business Transaction Verification-enabled Service Coordination Model

作　　者：袁敏[1,2] 黄志球[1] 李祥[1] 

机构地区：[1]南京航空航天大学信息科学与技术学院,南京210016 [2]湘南学院计算机科学系,湖南郴州423043

出　　处：《小型微型计算机系统》2011年第9期1734-1739,共6页Journal of Chinese Computer Systems

基　　金：国家"八六三"高技术研究发展计划项目(2009AA010307)资助;湖南省自然科学基金项目(09JJ3114)资助;湖南省教育厅重点项目(08A064)资助

摘　　要：在Web服务业务流程中如何保证参与者之间的协调一致性是亟待解决的重要问题.Web服务事务规范中描述的参与者之间的交互消息缺乏严格的语义,无法精确地描述复杂的协调活动,本文用Pi-演算形式化描述WS-TX规范中定义业务活动事务的WS-BA协议,在此基础上建立了适用于多方参与的业务事务的服务协调模型;并利用基于等价自动机转换的HAL模型检测工具,验证分析了WS-BA协议的安全性和活性,给出一个多方参与的业务事务实例的验证过程,介绍如何利用模型检测技术来分析业务流程设计正确性的方法,有效地确保了业务事务执行的可靠性和一致性.It is an urgent issue how to ensure distributed agreement among multiple-participants of service composition and business process. The definition of the message exchanges that take place between the process and each one of its partners in WS-TX OASIS Standard lacks the precise definition which is required for describing complex coordinated activities. This paper first models WS-Busi- hess Activity protocol （ WS-BA ） which specifies coordination types for long running loosely coupled business transactions. Second, proposes a service coordination model based on the formalization of the messaging interactions semantics in WS-BA using H-calculus. Then verifies system whether the protocol satisfies safety and liveness with HAL model checker. Finally, a case study of business transaction verification in multi-participants coordination is also presented, and introduces how to analyze the correctness of design for business process using model checking technology in order to efficiently guarantee the consistency and reliability of business transactions.

关 键 词：服务协调 业务流程 事务 形式化建模 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]