A model checker for WS-CDL

Service computing is becoming the prominent paradigm for distributed computing and electronic businesses. It enables developers to rapidly create their own software to meet the demands of their business processes, by composing existing services, especially Web services distributed on the Internet. WS-CDL is a W3C-proposed language for Web service composition, featuring the peer description of composite Web services amongst multiple participants. Since the traditional model checking methods based on the linear temporal logic (LTL) has limit in expressing the state-action relationship for a composite Web service model, this paper proposes a new approach, based upon the idea of Temporal Logic of Actions (TLA), to model check the composite Web services described in WS-CDL. In this paper, WS-CDL is extended by a new sub-language for expressing the temporal and action restriction properties, named TLA4CDL. The expressiveness of TLA4CDL is also discussed. The optimizing method called partial order reduction is introduced, followed by the discussion of the model checker algorithm. This leads to the development and implementation of the WS-CDL model checker. Finally, several test scenarios are provided in order to validate the WS-CDL model checker. The experimental results demonstrate this model checker is capable of detecting deadlock and verifying the specified constraint attributes by TLA4CDL. A comparison of experimental results with and without the partial order reduction method shows that our checker has better performance.