Abstract: To assure the correct and consistent execution of Web services, it is important to adopt a formal method to specify coordination processing in Web services. Based on the Web services transaction (WS-TX), an approach is proposed, which automatically models the coordination of multi-participants Web services from the business process execution language (BPEL). The rules of modeling the Web services coordination with Pi-calculus are discussed, then the method of obtaining coordination model of BPEL process is given with algorithm description, finally the effectiveness and correctness of the proposed approach are validated through a detailed case study.

Key words: Web service, coordination, Pi-calculus

摘要： 为了保证Web 服务组合执行获得正确一致的结果, 用形式化方法研究Web 服务事务处理的协调过程是很重要的。基于Web服务事务规范(Web services transaction, WS-TX), 提出了一种由业务流程执行语言(business process execution language, BPEL)自动生成Web服务多参与者协调事务模型的方法。介绍了Web服务协调的Pi-演算建模方法, 阐述了如何由BPEL描述的业务流程建立服务协调事务模型, 进一步给出了自动生成该协调模型的算法描述, 并通过具体实例说明了该方法的正确性及可行性。

关键词: Web服务, 协调, Pi-演算