Abstract: Web service choreography and orchestration defines the global interaction of composite Web service and the local behavior of each participant from global and local perspectives, respectively. The conformance of each participant's local behavior to global interaction is the guarantee of the correctness of Web service composition. The paper firstly presented a set of definitions to formally describe the global interaction of composite Web service, the local behavior of each participant and the mapping rules between them based on process algebra. Accordingly, two formal judgmental rules for the conformance of each participant's local behavior to global interaction were proposed. The two formal rules were based on the relationship between the transition of global interaction and local process and bisimulation theorem. At last, the conformance formal checking approach was described through a case study. The result of the case study shows that the proposed conformance definition of Web service composition and conformance checking approach can formally check the conformance of Web service composition effectively. As a result, the correctness of Web service composition can be guaranteed.

Key words: Web services composition, conformance test, Web services, formal method

摘要： Web服务编排和Web服务编制从全局和局部分别定义了Web服务组合的全局交互行为和每个参与者的局部行为,为了保证Web服务组合实现的正确性，Web服务组合的全局交互行为和每个参与者的局部行为必须是一致的。首先利用进程代数给出了对Web服务组合的全局交互行为、局部行为以及二者之间的映射关系的形式化描述，在此基础上分别通过分析全局会话变迁和局部进程变迁的关系和进程互相似理论给出了Web服务组合全局交互行为和局部行为的一致性的两个形式化判定准则。同时通过案例说明了如何形式化地检测Web服务组合的全局交互行为和局部行为之间的一致性。结果显示提出的Web服务组合一致性形式化定义和检测方法能检测组合行为的一致性，从而能有效地保证Web服务组合的正确性。

关键词: Web服务组合, 一致性检查, Web服务, 形式化方法