Verifying choreographic descriptions of web services based on CSP
Proceedings of the IEEE Services Computing Workshops, SCW 2006
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.
Copyright © 2006 IEEE. Access to external full text or publisher's version may require subscription.
Paper presented at the IEEE Services Computing Workshops (SCW 2006), 18-22 September 2006, Chicago, IL.
ISBN of the source publication: 9780769526812
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