Abstract | ||
---|---|---|
The Web Services Choreography Description Language (WS-CDL) is a W3C specification developed for the description of peer-to-peer collaborations of participants from a global viewpoint. Currently WS-CDL has no rigorous static type checking. We believe that introducing a type system will exclude many design and description errors, and ensure desirable properties of the choreography specifications. In this paper, we took a core language CDL, which covers most of the important features of the WS-CDL, and is more convenient for the study. We developed the abstract syntax and operational semantics of CDL, and defined a collection of rules which can be used to check if choreography is well-typed. Moreover, we also proved some type safety theorems for CDL in the sense that well-typed choreography cannot get stuck. We show how the use of type information can allow us to gain confidence in the correctness of choreography. |
Year | DOI | Venue |
---|---|---|
2006 | 10.1007/11901433_15 | ICFEM |
Keywords | Field | DocType |
type system,type safety,abstract syntax,operational semantics,choreography,web service | Operational semantics,Programming language,Type checking,Computer science,Correctness,Choreography,Abstract syntax,Core language,Type safety | Conference |
Volume | Issue | ISSN |
4260 LNCS | null | 0302-9743 |
ISBN | Citations | PageRank |
3-540-47460-9 | 11 | 0.87 |
References | Authors | |
8 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Hongli Yang | 1 | 191 | 14.80 |
Xiangpeng Zhao | 2 | 353 | 20.67 |
Zongyan Qiu | 3 | 436 | 41.04 |
Chao Cai | 4 | 145 | 8.48 |
Geguang Pu | 5 | 602 | 57.89 |