Algebraic Modeling and Verification of Web Service Composition

In order to provide a rigorous and sound foundation for formal reasoning about Web services, algebraic modeling is one of the important techniques used as is witnessed from the Web service literature. However, the algebraic modeling approach for Web services (Web service algebra) is still in its infancy. To further facilitate the algebraic modeling of Web services, in this paper, we propose a composition algebra based on the notion of recursive composition. The proposed algebra is fully capable to verify the presence of behavioral equivalences and deadlock conditions in a Web service composition scenario. The main motivation for proposing Web service composition algebra is to capture the recursive nature of composition which cannot be done using traditional approaches like model checking and Petri net.