A Calculus Of Web Services Choreography

Web services have gradually become an important field of research, both the industrial and academic worlds pay close attention to this topic. In order to guarantee that multiple Web services accomplish a highly complicated task in collaboration, people have come to pay more attentions to the concept of service choreography, that is, to describe behaviors and collaborations of multi-participants from a global viewpoint, in accomplishing a common business goal. WS-CDL is a language proposed by W3C for the specification of Web services choreography, whereas researchers pointed out that the language is still rather raw, and a number of problems remain to be solved well.The formal methods is an important effective investigation method for us to understand the essence of concurrent system. Since formal methods can be used to model and analyze concurrent systems for improving its correctness and reliability, it is natural to consider applying formal methods to the modelling and development of Web service area.This thesis studies the calculus of Web services choreography, with a special focus on the following aspects: a lightweight calculus is designed as the formal model for Web services choreography, and the corresponding semantics is defined. After giving the implementation model of choreography, we propose a set of projection rules from the global choreography model to the local implementation model, which can establish the correctness of implementation after projection. These investigations can help us to improve our understanding of the concepts of choreography and collaboration which are as the foundation of Web services and applications, and to have a better understanding of the problems related to the language design, implementation etc., and the essential issues of choreography.The main contributions of this dissertation are as following:1. The syntax and the semantics of the calculus of Web services choreography are defined. A set of operators is used to construct interaction of role processes, including the communication operator R(?)~cR, which is deadlock-free. We consider the meaning of a choreography as the set of all possible traces of its execution. The rules for the semantics are defined in trace set, specially, the emphasis is on synchronous communication, and the semantics of the parallel composition structure is denoted by interleaving activities of two traces. Based on the above calculus model, the structural congruence is defined as the least congruence relation including the expected structural laws for sequential composition, choice, and parallel composition. Furthermore, we also show that choreography will never deadlock.2. Inspired by influence of Orc, we combine the service oriented flavor of Orc with the name passing communication mechanism of theπ-calculus, and introduce the Orc_πcalculus as the implementation of choreographies. Since the concept of projection is proposed by us, together with a set of projection rules from the global choreography model to the local implementation model, we naturally find a set of structural conditions for specifying choreographies, and construct related axiomatic system. On this basis, we extend our calculus with some novel operators, and provide corresponding projection rules. Moreover, we give some examples to illustrate characteristics of the calculus, thus ensuring the correctness of projection and implementation for service choreographies.The above results are of profound theoretical and practical significance. In-depth studies of the phenomena appeared here can help us to explore the essence of choreography and various relative problems, and to lay solid foundation for further development of Web services. Meanwhile, the results of this study are of potential value for the web-based applications, thus providing technique and means for developmental tools of new-type Web services.