Abstract: To ensure the reliability of transaction execution in Web service business transaction, an approach to check the consistency of coordination actions among partner services was proposed. Aiming at the long-running transactions, a rigorous method by using Pi-calculus to calculate the service activities coordination in modeling business was put forward. The syntax mapping of automaton between Labeled Transition System(LTS)and Kripke structure was defined, and transformation from Pi-calculus process model to imput language of symbolic model checking was proposed. On the basis of test result, a counter-example was used to refine the model. Therefore the coordination problem of participants in business process integration was solved.The example was used to verity the effectiveness of proposed method.

Key words: business process integration, long-running transactions, service coordination, Pi-calculus, formal verification, Web services

摘要： 为有效地保证Web服务业务活动中事务可靠地执行，提出了一种检查伙伴服务之间协调行为一致性的方法。针对长事务给出用Pi-演算建模业务活动中服务协调行为的方法；定义了标号迁移系统和Kripke结构这两种状态自动机之间的语法映射关系，提出了Pi-演算进程模型到符号模型检测工具输入语言的转换方法；在模型检测结果的基础上，用反例引导用户进一步精化模型，以解决业务流程集成中参与者协调一致性问题。通过实例验证了该方法的有效性。

关键词: 业务流程集成, 长事务, 服务协调, Pi-演算, 形式化验证, Web服务