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

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

Recommended Citation

Yeung, W. L. (2007). CSP-based verification for web service orchestration and choreography. Simulation, 83(1), 65-74. doi: 10.1177/0037549707079227