Model Checking Interactions of Composite Web Services

There are two main challenges in the verification of composite webservices: 1) Asynchronous messaging makes most interesting problems undecid-able,and 2) rich data representation (XML) and data manipulation (e.g. XPathquery) forbids direct application of model checking tools. In this paper, we presenta top-down specification and verification approach to tackle both of these prob-lems.In our framework, each peer (individual web accessible program) interactswith other peers via asynchronous messages. We define a conversation among thepeers as the global sequence of messages exchanged by the peers. We propose atop-down approach where the set of desired conversations of a web service isspecified as a guarded automaton, which we call a conversation protocol. Guardsof the automata are XPath queries that manipulate message contents. We showthat if four realizability conditions are satisfied by a conversation protocol, theprojections of the protocol to each peer are guaranteed to preserve any LTL prop-ertiessatisfied by the protocol. We also present the translation from a guardedconversation protocol to a Promela specification that can be verified by the SPINmodel checker.