Verifying choreographic descriptions of web services based on CSP

Document Type

Conference paper

Source Publication

Proceedings of the IEEE Services Computing Workshops, SCW 2006

Publication Date


First Page


Last Page



IEEE Computer Society


Business process execution language, Choreography description language, CSP, Formal methods, Model checking


The emerging service-oriented architectures based on Web services is fostering a new generation of intra- and inter-organizational cross-platform Web-based business applications. With the new architectures comes a new set of standards (e.g. XML, SOAP, WSDL, UDDI) for enabling self-describing interoperable Web services, as well as for modeling and implementing workflow or process-oriented Web applications. The latter kind of standards include the Web Service Business Process Execution language (BPEL) and the Web Service Choreography Description Language (WS-CDL). While BPEL supports the modeling and implementation of a particular (composite) Web service, WS-CDL can be seen as a behavioral modeling language for the collaboration between multiple parties (Web services) within the same business process. In this paper, we outline how Communicating Sequential Processes (CSP) can be used as a formal basis for checking the behavioral consistency among the participants of a business process with respect to a choreography. The use of a model checking tool for automating the consistency checking is also discussed.



Publisher Statement

Copyright © 2006 IEEE. Access to external full text or publisher's version may require subscription.

Additional Information

Paper presented at the IEEE Services Computing Workshops (SCW 2006), 18-22 September 2006, Chicago, IL.

ISBN of the source publication: 9780769526812

Full-text Version

Publisher’s Version



Recommended Citation

Yeung, W. L., Wang, J., & Dong, W. (2006). Verifying choreographic descriptions of web services based on CSP. In Proceedings of the IEEE Services Computing Workshops, SCW 2006 (pp. 97-104). Los Alamitos: IEEE Computer Society. doi: 10.1109/SCW.2006.41