Model Verification Of Service-oriented Multi-participants Coordination

The reliability of Web services needs transaction. Due to some characteristics of Web services such as autonomy, flexibility, heterogeneous and so on, the traditional transaction semantics and protocols have proven to be inappropriate. As Web Services Transaction standard, WS-Transaction(WS-Tx) specifications define mechanisms for transactional interoperability between Web services domains and provide a means to compose transactional qualities of service into Web services applications. WS-Tx illustrates the abstract behavior of the protocol between a coordinator and a participant through the abstract state diagram, without giving the specific strategy for a coordinator with multiple participants. Nowadays, describing and verfying Web services composition and transaction is an important research direction, but current research mainly revolves around the modeling of transaction and protocols, rarely focuses on the behavior of coordination. So in this thesis, an approach of modeling and verifying service-oriented multi-participants coordination is proposed, the main research works can be listed as follows.First of all, the multi-participants coordination model of Web services based on WS-Tx protocol is proposed, which divides the dependency relations between participants into: Dominant, Dependent, Concurrent and Exclusion. According to each relation, the specific coordination strategy is given;Secondly, considering the formal method, Pi-calculus is adopted, and the mapping table and modeling rules from Web services coordination elements to Pi-calculus syntax are given in this dissertation. On the basis of mapping table between the coordination elements and Pi-calculus elemenets, the pi-calculus model of BPEL process can be obtained with algorithm description; After modeling of multi-participants coordination, safety and liveness are defined respectively in the coordination in terms of the dependency relations between the participants, which are then represented in CTL (Computation Tree Logic).Finally, a framework for verification of Pi-calculus based on NuSMV is presented. Besides, an instance of this framework is given, Flight Reservation, the effectiveness and correctness of the proposed approach in this thesis is validated.