Maude specification of web service composition and adaptation

Web services composition is emerging as a new model for automated interactions among distributed and heterogeneous applications. However the reuse of web services raises composition issues since they present, most of the time, mismatching at different levels such as structural, behavioral and non-functional. The resulted mismatches require adaptation to insure the correct working between web services. In this paper we present a formal specification of operations which enable to compose and adapt services at runtime. This specification is given in Maude language as a logical framework. Thanks to many Maude tools, formal analysis may be easily performed.