Paper Info
Title
Towards the Formal Model and Verification of Web Service Choreography Description Language
Abstract
The Web Services Choreography Description Language (WS-CDL) is a W3C specification for the description of peer-to-peer collaborations of participants from a global viewpoint. For the rigorous development and tools support for the language, the formal semantics of WS-CDL is worth investigating. This paper proposes a small language CDL as a formal model of the simplified WS-CDL, which includes important concepts related to participant roles and collaborations among them in a choreography. The formal operational semantics of CDL is given. Based on the formal model, we discuss further: 1) project a given choreography to orchestration views, which provides a basis for the implementation of the choreography by code generation; 2) translate WS-CDL to the input language of the model-checker SPIN, which allows us to automatically verify the correctness of a given choreography. An automatic translator has been implemented.
Year
DOI
Venue
2006
10.1007/11841197_18
Web Services and Formal Methods
Keywords
DocType
Volume
operational semantics,code generation,formal semantics,web service
Conference
4184
ISSN
ISBN
Citations 
16113349
3-540-38862-1
27
PageRank 
References 
Authors
1.68
14
3
Name
Order
Citations
PageRank
Xiangpeng Zhao135320.67
Hongli Yang219114.80
Zongyan Qiu343641.04