Formal description and analysis of conformance of composite Web service behavior
Xiang Jun · Journal of Computer Applications · 2012
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.