Towards a formal framework for choreography

One of the main challenges in the area of service oriented computing, in general, and of Web services technology, in particular, is the definition of languages and models for the description of choreographies. A choreography defines the collaborations between interacting services: more precisely, it specifies a contract containing a "global" definition of the common ordering conditions and constraints under which messages are exchanged in a services conversation. In this paper, starting from the analysis of the main aspects of Web services technology, we propose a simple choreography language, equipped with a formal semantics, which is intended as the starting point for the development of a framework for the design and analysis of choreographies in service oriented computing.