Research On Formal Verification Of Web Services Flow Based On Pi-Calculus

To meet the rapid change of enterprise business requirements, SOA (service-oriented architecture), a new software architecture, is presented, and leads a technological revolution of software industry. Web service is the basic component of SOA, which is used to construct distributed, loose-coupled enterprise-scale application systems on demand. A single Web service can only provide limited functions. In order to share Web services on the Internet, it is very essential to combine the existing services into composite service or information system.Verification of Web services composition is to find the problems of the composition before deployment, which is the key for Web services composition becomes practical. This thesis, which is based on National Support plan and 863 research projects of our lab, emphasizes the formal verification of Web services flow. The major work has three parts:1. Pi-calculus-based Modeling of SFDL. Pi-calculus is a powerful and brief formal method, which is fit to model the loose-coupled, concurrent and distributed systems. Firstly, general flow patterns are modeled by Pi-calculus. Then it introduces a new services composition language: SFDL (Service Flow Definition Language), which is based on the BPEL and XPDL. SFDL, which is based on XML, is easy to understand. According to the characteristics of SFDL, we present algorithms based on modes for Pi-calculus-based Modeling of SFDL.2. Pi-calculus-based verification of Web services flow. The research scope of verification of Web services flow includes reachable of activities, deadlock, live lock and so on. This thesis verifies the problems of Web services flow with the operational semantics, automatic deductive of Pi-calculus. The processes with problems will not be deductive to a NULL process. It introduces how to use MWB to automated verification and its advantages and disadvantages. To integrate with existing systems and solve other problems, methods and algorithms are presented to improve automated verification. The solution is deducing the processes of Pi-calculus in our systems and verifying these processes states during deduction.3. Prototype of Pi-calculus-based verification of Web services flow. It introduces WSCF (Web Service Composition Framework) and its prototype - JTangFlow-S. And JTangFlow-S implements the algorithms about Pi-calculus-based verification of Web services flow. Experiments show these algorithms are practical.