Synchronizability of conversations among Web services

We present a framework for analyzing interactions among Web services that communicate with asynchronous messages. We model the interactions among the peers participating in a composite Web service as conversations, the global sequences of messages exchanged among the peers. This naturally leads to the following model checking problem: Given an LTL property and a composite Web service, do the conversations generated by the composite Web service satisfy the property? We show that asynchronous messaging leads to state space explosion for bounded message queues and undecidability of the model checking problem for unbounded message queues. We propose a technique called synchronizability analysis to tackle this problem. If a composite Web service is synchronizable, its conversation set remains the same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite Web services with unbounded message queues can be verified completely using a finite state model checker such as SPIN. We also show that synchronizability analysis can be used to check the reliability of top-down conversation specifications and we contrast the conversation model with the Message Sequence Charts. We integrated synchronizability analysis to a tool we developed for analyzing composite Web services.