CDLChecker: A WS-CDL analysis tool

This paper presents a tool for the analysis of WS-CDL, which gives a global view on the collaboration among a collection of services involving multiple different organizations for independent processes. This tool is named by CDLChecker with providing three functionalities. The first one is the simulation of real WS-CDL programs. The CDLChecker can simulate the execution of WSCDL programs involving Web services provided by the third-party, where external variable definitions are resolved by an XML parser we designed. The second one is to validate the constraints specified in WS-CDL specification. The static and dynamic constraints are specified by abstract machines from B method, and the corresponding validation algorithm is integrated into this tool. The last part of this tool can verify the user-related properties of service choreography, such as channel absence and channel redundancy. The back-end verification engine we used here is the Spin model checker.