MODEL AND VERIFICATION OF WS-CDL BASED ON UML DIAGRAMS

The Web Services Choreography Description Language (WS-CDL) is a specification developed by the W3C and can be viewed as a blueprint for the development of endpoint services. Consequently, it is worth providing a systematic approach for its modeling, analysis and verification. The Unified Modeling Language (UML) is an industry standard for modeling. Applying UML to model WS-CDL is obviously a promising solution to bring together academics and practitioners through a unique standard language. In this paper, we propose to use different UML diagrams to model WS-CDL. UML Component Diagram is used to model the underlying structure of WS-CDL. UML Sequence Diagram is utilized to model the activities in WS-CDL. UML State Machine Diagram is utilized to model the behaviors of each role participating in a WS-CDL specification. We then enrich the UML State Machine Diagram with data by the use of UML Class Diagram. Given the UML specification of WS-CDL, we then provide a systematic way of formally analyzing and verifying WS-CDL against desired properties. Some experiments show that our approach can verify structural, behavioral and data properties in a middle-scale data-enriched WS-CDL specification.