Formal Analysis And Verification Of A Transaction Coordination Protocol Named Ws-tx For Web Services

As a new computing model, Web Services are becoming more and more attractive. It is one of the most important challenges of Web Services to ensure that the result of running composited web services is consistent and reliable. Transaction mechanism is considered to be applied in web services composition to generate consistent and reliable outcome. Nowadays, new transaction protocols and standards based on traditional transaction mechanisms are proposed in consideration of Web Services'characteristics such as autonomy, heterogeneous, long period and so on. Among the protocols, a coordination protocol named WS-TX is a commonly concerned protocol for it has used the existing and developing standards and can be actioned as a component in the web services architecture.As we know that WS-TX is described by natural language and lacks of strict semantics, lots of researchers apply formal method to do research on WS-TX. Howerver, the correctness of protocol doesn't imply that the scenarios applying WS-TX meet transaction needs. Thus pi-calculus is used to model the scenarios applying WS-TX and a symbolic model checking tool named NuSMV2 is adopted to check whether the scenarios meet safety and liveness. The main research works can be listed as follows.First of all, considering the concurrency of WS-TX scenarios, pi-calculus is adopted and the mapping relation of elements of WS-TX scenarios and pi-calculus is proposed. Furthermore, modeling rules of pi-calculus are studied. In order to verify the practicability of mapping rules, a scenario about account transfer applying WS-AT which is a concrete coordination protocol in WS-TX and another scenario about travel arrangement applying WS-BA which is another coordination protocol in WS-TX are presented and modeled by pi-calculus.Secondly, for existing model checking tools for pi-calculus can't meet our command, pi-calculus models are translated into finite state machine described by SMV language, which is the input of NuSMV2. The translating rules from pi-calculus models to SMV language code are proposed derived from the mapping from labeled transition system to kripke structure. Based on the rules, an automatic translating tool named PiCal2NuSMV is designed and implemented.Finally, safety and liveness are defined respectively in WS-AT scenarios and WS-BA scenarios, which are then represented in CTL (Computation Tree Logic). NuSMV2 is used to checking whether the coordination processes of account transfer and travel arrangement meet the properties described in CTL. The result of model checking shows that the scenarios applying WS-TX have transaction properties and the WS-TX protocol itself is reliable. A method about how to analyse conuterexamples generated by NuSMV2 is presented lastly.