Set Partition and Trace Based Verification of Web Service Composition

De*signing and running Web services compositions are error-prone as it is difficult to determine the behavior of web services during execution and their conformance to functional requirements. Interaction among composite Web services may cause concurrency related issues. In this paper, we present a formal model for reasoning and verifying Web services composition at design level. We partition the candidate services being considered for composition into several subsets on the basis of their service invocation order. We arrange these subsets to form a Web services set partition graph and transform to a set of interacting traces. Then, we propose a novel methodology for service interaction verification that uses service description (from WSDL file) to extract the necessary information and facilitates the process of modeling, analyzing, and reasoning the composite services. As a part of verification technique, we use two levels of modeling. This includes abstract modeling that further leads to detailed modeling if required, thereby reducing the computation time and modeling complexity.