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.
Bibliographical notePaper presented at the IEEE Services Computing Workshops (SCW 2006), 18-22 September 2006, Chicago, IL.
ISBN of the source publication: 9780769526812
- Business process execution language
- Choreography description language
- Formal methods
- Model checking