NDLI: Model-Checking of Web Services Choreography

Content Provider	IEEE Xplore Digital Library
Author	Yang Hongli Zhao Xiangpeng Cai Chao Qiu Zongyan
Copyright Year	2008
Description	Author affiliation: Dept. of Inf., Peking Univ., Beijing, China (Zhao Xiangpeng; Cai Chao; Qiu Zongyan) \|\| Coll. of Comput. Sci., Beijing Univ. of Technol., Beijing, China (Yang Hongli)
Abstract	Web services choreography describes the global model of service interactions among a set of participants. In order to achieve a common business goal, the protocols of interaction must be correct. In this paper, we model interactions with recordings of state/channel variable changes that can occur as a result of carrying out the interactions. Thus, it is possible to verify not only normal control flow properties such as deadlock-freeness, but also channel-passing related problems such as channel-absence. Concretely, we propose a small language CDL, together with an operational semantics. We illustrate with a T-Shirts procurement protocol how service choreographies can be specified in CDL, and how the verification can be carried out using the SPIN model-checker.
Starting Page	79
Ending Page	84
File Size	206988
Page Count	6
File Format	PDF
ISBN	9780769534992
DOI	10.1109/SOSE.2008.40
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2008-12-18
Publisher Place	Taiwan
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Procurement Chaos Protocols WS-CDL Choreography Educational institutions Application software Web services CD recording Systems engineering and theory Computer science education Informatics Model-checking
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A Formal Model forWeb Service Choreography Description Language (WS-CDL)

Verification of channel passing in choreography with model checking

Verifying WS-CDL-Based Web Services Collaboration by Model Checking

LTSA-WS: a tool for model-based verification of web service compositions and choreography

Reasoning about Channel Passing in Choreography

CDLChecker: A WS-CDL analysis tool

A calculus for WS-CDL language

Bptrends march 2005 a critical overview of ws-cdl a critical overview of the web services choreography description language (ws-cdl).

A Comparative Study between WSCI, WS-CDL, and OWL-S

Model-Checking of Web Services Choreography

Similar Documents

A Formal Model forWeb Service Choreography Description Language (WS-CDL)

Verification of channel passing in choreography with model checking

Verifying WS-CDL-Based Web Services Collaboration by Model Checking

LTSA-WS: a tool for model-based verification of web service compositions and choreography

Reasoning about Channel Passing in Choreography

CDLChecker: A WS-CDL analysis tool

A calculus for WS-CDL language

Bptrends march 2005 a critical overview of ws-cdl a critical overview of the web services choreography description language (ws-cdl).

A Comparative Study between WSCI, WS-CDL, and OWL-S

Model-Checking of Web Services Choreography