@inproceedings{c3fc5b4548c04864b035663515f39d0a,
title = "Type checking choreography description language",
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.",
keywords = "Choreography, Formal model, Type checking, WS-CDL",
author = "Yang Hongli and Zhao Xiangpeng and Qiu Zongyan and Cai Chao and Pu Geguang",
year = "2006",
language = "英语",
isbn = "3540474609",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "264--283",
booktitle = "Formal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings",
address = "德国",
note = "8th International Conference on Formal Engineering Methods, ICFEM 2006 ; Conference date: 01-11-2006 Through 03-11-2006",
}