摘要
在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.
出处
《小型微型计算机系统》
CSCD
北大核心
2011年第9期1734-1739,共6页
Journal of Chinese Computer Systems
基金
国家"八六三"高技术研究发展计划项目(2009AA010307)资助
湖南省自然科学基金项目(09JJ3114)资助
湖南省教育厅重点项目(08A064)资助
关键词
服务协调
业务流程
事务
形式化建模
service coordination
business process
transactions
formal modeling