Type Checking Choreography Description Language

  • Hongli Yang
  • Xiangpeng Zhao
  • Zongyan Qiu
  • Chao Cai
  • Geguang Pu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


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.


Choreography WS-CDL Formal model Type checking 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. In: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (1999)Google Scholar
  2. 2.
    Austin, D., Barbir, A., Peters, E., Ross-Talbot, S.: Web Services Choreography Requirements. W3C Working Draft (March 2004),
  3. 3.
    Barros, A., Dumas, M., Oaks, P.: A Critical Overview of the Web Services Choreography Description Language (2005),
  4. 4.
    Brogi, A., Canal, C., Pimentel, E., Vallecillo, A.: Formalizing web service choreography. In: WS-FM 2004. Electronic Notes in Theoretical Computer Science (2004)Google Scholar
  5. 5.
    Busi, N., Gorrieri, R., Guidi, C., Lucchi, R., Zavattaro, G.: Towards a formal framework for Choreography. In: Proceedings of the 14th IEEE International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprise. IEEE Computer Society, Los Alamitos (2005)Google Scholar
  6. 6.
    Draper, D., et al.: XQuery 1.0 and XPath 2.0 Formal Semantics. W3C Working Draft (September 2005),
  7. 7.
    Holzmann, G.J.: The SPIN Model Checker:Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  8. 8.
    Yang, H., Zhao, X., Qiu, Z., Pu, G., Wang, S.: A Formal Model for Web Service Choreography Description Language (WS-CDL). In: Proceedings of International Conference on Web Services(ICWS) (to appear, 2006)Google Scholar
  9. 9.
    Hosoya, H., Pierce, B.C.: XDuce: A Statically Typed XML Processing Language (May 2003),
  10. 10.
    Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y., Barreto, C.: Web Services Choreography Description Language Version 1.0. (November 2005),
  11. 11.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)Google Scholar
  12. 12.
    Ross-Talbot, S., Fletcher, T.: Web Services Choreography Description Language: Primer Version 1.0 (May 2006),
  13. 13.
    Zhao, X., Yang, H., Qiu, Z.: Towards the Formal Model and Verification of Web Service Choreography Description Language. In: Proceedings of 3rd International Workshop on Web Services and Formal Methods(WS-FM) (to appear, 2006)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Hongli Yang
    • 1
  • Xiangpeng Zhao
    • 1
  • Zongyan Qiu
    • 1
  • Chao Cai
    • 1
  • Geguang Pu
    • 2
  1. 1.LMAM and Department of Informatics, School of Math.Peking UniversityBeijingChina
  2. 2.Software Engineering InstituteEast China Normal UniversityShanghaiChina

Personalised recommendations