Title
CSP-based verification for web service orchestration and choreography
Document Type
Journal article
Source Publication
SIMULATION
Publication Date
1-1-2007
Volume
83
Issue
1
First Page
65
Last Page
74
Publisher
Sage Publications Ltd.
Keywords
Web services, choreography, orchestration, formal methods, model checking, CSP
Abstract
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.
DOI
10.1177/0037549707079227
Print ISSN
00375497
E-ISSN
17413133
Publisher Statement
Copyright © Simulation Councils Inc.
Access to external full text or publisher's version may require subscription.
Full-text Version
Publisher’s Version
Language
English
Recommended Citation
Yeung, W. L. (2007). CSP-based verification for web service orchestration and choreography. Simulation, 83(1), 65-74. doi: 10.1177/0037549707079227
