CSP-based verification for web service orchestration and choreography

Wing Lok YEUNG

Research output: Journal PublicationsJournal Article (refereed)

10 Citations (Scopus)

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.
Original languageEnglish
Pages (from-to)65-74
Number of pages10
JournalSimulation
Volume83
Issue number1
DOIs
Publication statusPublished - 1 Jan 2007

Fingerprint

Choreography
Orchestration
Web services
Web Services
Business Process
WSDL
Industry
Behavioral Modeling
Interoperability
Service-oriented Computing
Software Components
Modeling Language
Work Flow
Language
Network protocols

Keywords

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

Cite this

YEUNG, Wing Lok. / CSP-based verification for web service orchestration and choreography. In: Simulation. 2007 ; Vol. 83, No. 1. pp. 65-74.
@article{37faa1bb1d464d17a9fd4da6765465ea,
title = "CSP-based verification for web service orchestration and choreography",
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.",
keywords = "CSP, Web services, choreography, formal methods, model checking, orchestration",
author = "YEUNG, {Wing Lok}",
year = "2007",
month = "1",
day = "1",
doi = "10.1177/0037549707079227",
language = "English",
volume = "83",
pages = "65--74",
journal = "Simulation",
issn = "0037-5497",
publisher = "SAGE Publications Ltd",
number = "1",

}

CSP-based verification for web service orchestration and choreography. / YEUNG, Wing Lok.

In: Simulation, Vol. 83, No. 1, 01.01.2007, p. 65-74.

Research output: Journal PublicationsJournal Article (refereed)

TY - JOUR

T1 - CSP-based verification for web service orchestration and choreography

AU - YEUNG, Wing Lok

PY - 2007/1/1

Y1 - 2007/1/1

N2 - 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.

AB - 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.

KW - CSP

KW - Web services

KW - choreography

KW - formal methods

KW - model checking

KW - orchestration

UR - http://commons.ln.edu.hk/sw_master/180

U2 - 10.1177/0037549707079227

DO - 10.1177/0037549707079227

M3 - Journal Article (refereed)

VL - 83

SP - 65

EP - 74

JO - Simulation

JF - Simulation

SN - 0037-5497

IS - 1

ER -