Verifying choreographic descriptions of web services based on CSP

Wing Lok YEUNG, Ji WANG, Wei DONG

Research output: Book Chapters | Papers in Conference ProceedingsConference paper (refereed)Researchpeer-review

5 Citations (Scopus)

Abstract

The emerging service-oriented architectures based on Web services is fostering a new generation of intra- and inter-organizational cross-platform Web-based business applications. With the new architectures comes a new set of standards (e.g. XML, SOAP, WSDL, UDDI) for enabling self-describing interoperable Web services, as well as for modeling and implementing workflow or process-oriented Web applications. The latter kind of standards include the Web Service Business Process Execution language (BPEL) and the Web Service Choreography Description Language (WS-CDL). While BPEL supports the modeling and implementation of a particular (composite) Web service, WS-CDL can be seen as a behavioral modeling language for the collaboration between multiple parties (Web services) within the same business process. In this paper, we outline how Communicating Sequential Processes (CSP) can be used as a formal basis for checking the behavioral consistency among the participants of a business process with respect to a choreography. The use of a model checking tool for automating the consistency checking is also discussed.
Original languageEnglish
Title of host publicationProceedings of the IEEE Services Computing Workshops, SCW 2006
PublisherIEEE Computer Society
Pages97-104
Number of pages8
DOIs
Publication statusPublished - 1 Jan 2006

Fingerprint

Web services
WSDL
Industry
Model checking
Service oriented architecture (SOA)
XML
Composite materials

Bibliographical note

Paper presented at the IEEE Services Computing Workshops (SCW 2006), 18-22 September 2006, Chicago, IL.
ISBN of the source publication: 9780769526812

Keywords

  • Business process execution language
  • CSP
  • Choreography description language
  • Formal methods
  • Model checking

Cite this

YEUNG, W. L., WANG, J., & DONG, W. (2006). Verifying choreographic descriptions of web services based on CSP. In Proceedings of the IEEE Services Computing Workshops, SCW 2006 (pp. 97-104). IEEE Computer Society. https://doi.org/10.1109/SCW.2006.41
YEUNG, Wing Lok ; WANG, Ji ; DONG, Wei. / Verifying choreographic descriptions of web services based on CSP. Proceedings of the IEEE Services Computing Workshops, SCW 2006. IEEE Computer Society, 2006. pp. 97-104
@inproceedings{1808d08db29d48d9be99dafea7878e52,
title = "Verifying choreographic descriptions of web services based on CSP",
abstract = "The emerging service-oriented architectures based on Web services is fostering a new generation of intra- and inter-organizational cross-platform Web-based business applications. With the new architectures comes a new set of standards (e.g. XML, SOAP, WSDL, UDDI) for enabling self-describing interoperable Web services, as well as for modeling and implementing workflow or process-oriented Web applications. The latter kind of standards include the Web Service Business Process Execution language (BPEL) and the Web Service Choreography Description Language (WS-CDL). While BPEL supports the modeling and implementation of a particular (composite) Web service, WS-CDL can be seen as a behavioral modeling language for the collaboration between multiple parties (Web services) within the same business process. In this paper, we outline how Communicating Sequential Processes (CSP) can be used as a formal basis for checking the behavioral consistency among the participants of a business process with respect to a choreography. The use of a model checking tool for automating the consistency checking is also discussed.",
keywords = "Business process execution language, CSP, Choreography description language, Formal methods, Model checking",
author = "YEUNG, {Wing Lok} and Ji WANG and Wei DONG",
note = "Paper presented at the IEEE Services Computing Workshops (SCW 2006), 18-22 September 2006, Chicago, IL. ISBN of the source publication: 9780769526812",
year = "2006",
month = "1",
day = "1",
doi = "10.1109/SCW.2006.41",
language = "English",
pages = "97--104",
booktitle = "Proceedings of the IEEE Services Computing Workshops, SCW 2006",
publisher = "IEEE Computer Society",
address = "United States",

}

YEUNG, WL, WANG, J & DONG, W 2006, Verifying choreographic descriptions of web services based on CSP. in Proceedings of the IEEE Services Computing Workshops, SCW 2006. IEEE Computer Society, pp. 97-104. https://doi.org/10.1109/SCW.2006.41

Verifying choreographic descriptions of web services based on CSP. / YEUNG, Wing Lok; WANG, Ji; DONG, Wei.

Proceedings of the IEEE Services Computing Workshops, SCW 2006. IEEE Computer Society, 2006. p. 97-104.

Research output: Book Chapters | Papers in Conference ProceedingsConference paper (refereed)Researchpeer-review

TY - GEN

T1 - Verifying choreographic descriptions of web services based on CSP

AU - YEUNG, Wing Lok

AU - WANG, Ji

AU - DONG, Wei

N1 - Paper presented at the IEEE Services Computing Workshops (SCW 2006), 18-22 September 2006, Chicago, IL. ISBN of the source publication: 9780769526812

PY - 2006/1/1

Y1 - 2006/1/1

N2 - The emerging service-oriented architectures based on Web services is fostering a new generation of intra- and inter-organizational cross-platform Web-based business applications. With the new architectures comes a new set of standards (e.g. XML, SOAP, WSDL, UDDI) for enabling self-describing interoperable Web services, as well as for modeling and implementing workflow or process-oriented Web applications. The latter kind of standards include the Web Service Business Process Execution language (BPEL) and the Web Service Choreography Description Language (WS-CDL). While BPEL supports the modeling and implementation of a particular (composite) Web service, WS-CDL can be seen as a behavioral modeling language for the collaboration between multiple parties (Web services) within the same business process. In this paper, we outline how Communicating Sequential Processes (CSP) can be used as a formal basis for checking the behavioral consistency among the participants of a business process with respect to a choreography. The use of a model checking tool for automating the consistency checking is also discussed.

AB - The emerging service-oriented architectures based on Web services is fostering a new generation of intra- and inter-organizational cross-platform Web-based business applications. With the new architectures comes a new set of standards (e.g. XML, SOAP, WSDL, UDDI) for enabling self-describing interoperable Web services, as well as for modeling and implementing workflow or process-oriented Web applications. The latter kind of standards include the Web Service Business Process Execution language (BPEL) and the Web Service Choreography Description Language (WS-CDL). While BPEL supports the modeling and implementation of a particular (composite) Web service, WS-CDL can be seen as a behavioral modeling language for the collaboration between multiple parties (Web services) within the same business process. In this paper, we outline how Communicating Sequential Processes (CSP) can be used as a formal basis for checking the behavioral consistency among the participants of a business process with respect to a choreography. The use of a model checking tool for automating the consistency checking is also discussed.

KW - Business process execution language

KW - CSP

KW - Choreography description language

KW - Formal methods

KW - Model checking

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

U2 - 10.1109/SCW.2006.41

DO - 10.1109/SCW.2006.41

M3 - Conference paper (refereed)

SP - 97

EP - 104

BT - Proceedings of the IEEE Services Computing Workshops, SCW 2006

PB - IEEE Computer Society

ER -

YEUNG WL, WANG J, DONG W. Verifying choreographic descriptions of web services based on CSP. In Proceedings of the IEEE Services Computing Workshops, SCW 2006. IEEE Computer Society. 2006. p. 97-104 https://doi.org/10.1109/SCW.2006.41