Title :
Mapping WS-CDL and BPEL into CSP for Behavioural Specification and Verification of Web Services
Author_Institution :
Dept. of Comput. & Decision Sci., Lingnan Univ., Tuen Mun
Abstract :
The Web service Business Process Execution Language (WS-BPEL) and the Web service Choreography Description Language (WS-CDL) are two important standards for modelling and implementing workflows and business processes based on Web services. From the WS-CDL description of a Web services based business process, we may extract a behavioural specification against which the combined behaviour of the participating Web services should be verified. We show how to express this behavioural specification as well as the behaviour of individual WS-BPEL-based Web services in the formalism of communicating sequential processes (CSP), which supports a formal approach to verifying the behaviour of collaborating Web services
Keywords :
Web services; communicating sequential processes; formal specification; formal verification; specification languages; WS-BPEL; WS-CDL description; Web service Business Process Execution Language; Web service Choreography Description Language; behavioural specification; behavioural verification; communicating sequential processes; formal methods; model checking; workflows; Availability; Collaboration; Information systems; Process design; Service oriented architecture; Simple object access protocol; Software design; Unified modeling language; Web services; XML; CSP.; Choreography description language; business process execution language; formal methods; model checking;
Conference_Titel :
Web Services, 2006. ECOWS '06. 4th European Conference on
Conference_Location :
Zurich
Print_ISBN :
0-7695-2737-X
DOI :
10.1109/ECOWS.2006.26
