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

Business Transaction Verification-enabled Service Coordination Model

在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.