Towards a formal foundation to choreography languages

We introduce a formal framework for studying the semantics of choreography languages for Web Services. Taking WS-CDL language as reference case study, we define syntax and semantics of a core language to derive the collaborations of participants from a WS-CDL specification. Based on the formal model, we discuss further: (1) projection from a given choreography to orchestration views, which provides a basis for the implementation of the choreography; (2) correctness of projection, in the sense that it ensures the parallel composition of the generated role processes will be an implementation of the choreography. A useful Equation is given.