This Article Full Text (PDF) References Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Similar articles in ISI Web of Science Alert me to new issues of the journal Add to Saved Citations Download to citation manager Add to My Marked Citations Citing Articles Citing Articles via Google Scholar Google Scholar Articles by Yeung, W.L. Search for Related Content Social Bookmarking                   What's this?

CSP-Based Verification for Web Service Orchestration and Choreography

Lingnan University Hong Kong, wlyeung{at}ln.edu.hk

Service-oriented computing aspires to an unprecedented level of platform-independence and inter-operability 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.

Key Words: Web services • choreography • orchestration • formal methods • model checking • CSP

CiteULike    Connotea    Del.icio.us    Digg    Reddit    Technorati    What's this?