Verifying WS-CDL-Based Web Services Collaboration by Model Checking

WS-CDL is a W3C-proposed formal language for Web service collaboration, featuring the peer description of composite Web services amongst multiple participants. After describing the Web Service Collaboration in WS-CDL, it is important to ensure its satisfaction of certain attributes by formal verification. This paper proposes an new language, namely TLA4CDL to express the temporal and action attributes in WS-CDL, which is actually based on the idea of the temporal logic of actions, and an algorithm to model check the WS-CDL choreography in TLA4CDL. We will first extend WS-CDL with the new language, TLA4CDL for expressing the temporal and action attributes, and analyzing its technology benefits as well as its expressiveness. Then, an algorithm to model check WS-CDL in TLA4CDL will be introduced, the optimizing method called partial order reduction will be presented, and the complexity of this algorithm will be discussed, all of which lead the way to the implementation of a WS-CDL model checker. At last, experiment cases are designed to show the validation of the WS-CDL model checker on TLA4CDL.