A Semantic Framework for Analyzing Web Services Composition

Service oriented architecture (SOA) is an emergent paradigm that aims at building applications and components by assembling existing ones. Several works on composition aspects have been proposed by researchers and industrial practitioners. The overall observation about these works is that they only provide means for service composition and invocation; but, they offer little support for analysis, and formal checking of composite Web services. In this work, we exploit rewriting logic as a unique semantic formalism for well describing and checking Web services composition. Thanks to this formalization we lean on the category model to give precise and sufficient semantics to Web service behavior. Besides, this high level specification constitutes an executable one, it allows formal analysis using a particular wellfounded language Maude having a proof and prototyping environment. General Terms Formal Methods, Web Services.