Verifying choreographic descriptions of web services based on CSP


Research output: Book Chapters | Papers in Conference ProceedingsConference paper (refereed)Researchpeer-review

5 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationProceedings of the IEEE Services Computing Workshops, SCW 2006
PublisherIEEE Computer Society
Number of pages8
Publication statusPublished - 1 Jan 2006

Bibliographical note

Paper 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
  • CSP
  • Choreography description language
  • Formal methods
  • Model checking


Dive into the research topics of 'Verifying choreographic descriptions of web services based on CSP'. Together they form a unique fingerprint.

Cite this