论文部分内容阅读
在Web服务业务流程中如何保证参与者之间的协调一致性是亟待解决的重要问题.Web服务事务规范中描述的参与者之间的交互消息缺乏严格的语义,无法精确地描述复杂的协调活动,本文用Pi-演算形式化描述WS-TX规范中定义业务活动事务的WS-BA协议,在此基础上建立了适用于多方参与的业务事务的服务协调模型;并利用基于等价自动机转换的HAL模型检测工具,验证分析了WS-BA协议的安全性和活性,给出一个多方参与的业务事务实例的验证过程,介绍如何利用模型检测技术来分析业务流程设计正确性的方法,有效地确保了业务事务执行的可靠性和一致性.
How to ensure the consistency of participants in Web service business processes is an important issue that needs to be solved urgently.The interactive messages among the participants described in the Web Services business rules lack of strict semantics and can not accurately describe complex coordination activities , This paper formally describes the WS-BA protocol that defines business activity in the WS-TX specification with P-calculus. Based on the WS-BA protocol, a service coordination model that is suitable for multi-participant business transactions is established. Based on equivalent automaton transformation HAL model checking tool, verifies and analyzes the security and activity of WS-BA protocol, gives a multi-participative example of business transaction verification process, introduces how to use model checking technology to analyze the correctness of business process design, and effectively Ensuring the reliability and consistency of business execution.