CSP-based verification for web service orchestration and choreography

Wing Lok YEUNG

Research output: Journal PublicationsJournal Article (refereed)peer-review

11 Citations (Scopus)


Service-oriented computing aspires to an unprecedented level of platform-independence and interoperability of software components for intra- and inter-organizational business processes through standard protocols and languages for workflows and process-oriented applications. The Web Service Business Process Execution Language (WS-BPEL) and the Web Service Choreography Description Language (WS-CDL) are two major languages for modeling and implementing Web services-based business processes. A Web service can be modeled in WS-BPEL by an abstract process describing its external behavior in terms of message exchanges with other participants (Web services). The abstract process can then be refined with more details to become an executable process. On the other hand, WS-CDL serves as a behavioral modeling language for the collaboration between multiple participants (Web services) within the same business process from a global point of view. In this paper, we outline how Communicating Sequential Processes (CSP) can be used as a formal basis for verifying the behavioral consistency among abstract and executable processes together with choreographic descriptions.
Original languageEnglish
Pages (from-to)65-74
Number of pages10
Issue number1
Publication statusPublished - 1 Jan 2007


  • CSP
  • Web services
  • choreography
  • formal methods
  • model checking
  • orchestration


Dive into the research topics of 'CSP-based verification for web service orchestration and choreography'. Together they form a unique fingerprint.

Cite this