Modeling And Verification Of Web Service Composition

Web service is a kind of application that based on service-oriented computing. Many heterogeneous, multi-platform, developed by different developers Web applications combines to a new Web service, by using different logic control flow. Since the theory of Web service was presented, it had caused widespread concern from the industry. However, the massive Web composite services combined by many heterogeneous Web services, it’s very difficult to guarantee its security about control flow. Therefore this thesis aims at this problem, regards the system as a multi-agents knowledge logic system, using the model checking methods to verify the security of massive Web composite service.In this thesis, we at first introduce relevant basic knowledge and technology. Then we summary the current research of model verification of Web service. In the thied part of this thesis, we present a point that regards the massive Web composite service as a multi-agent knowledge logic system. We prove its feasibility and give the transition tuples of BPEL language activities. Then, in order to enhance model detection ability for large-scale systems and solve the problem of state space explosion, we describe a new model checking algorithm that use disk database to manage the system state. The new algorithm based on the breadth-first search algorithm, using the database to reduce system state in each layer. And we add a hash algorithm to decrease times of IO operations, so the model checker can handle and verify the massive system and return all possible counterexample in an acceptable time and storage consumption. At the end of this thesis, we implement this algorithm and give the Promela form of the electronic commerce from daily life as model checking example. Then we introduce method transforms multi-agent knowledge logic into linear temporal logic, LTL. We input the example in our algorithm and other three model checkers and contrast their output and their expression.This thesis focus on two aspects: modeling and algorithm implementation.we firstly present a model checking method to handle large-scale system and return its all counterexample. And then we regard the massive Web composite service as a multi-agent knowledge logic model. In this mehod, we can verify the multi-agent knowledge property of a massive Web service successfully. From the comparison of four detection algorithms, we can prove that our algorithm can verify the multi-agent knowledge logic property and has a better performance in handling a large-scale model. Our algorithm can find all possible counterexamples from a large-scale system in the acceptable time and storage consumption. And it can verify the multi-agent knowledge logic property from a massive Web composite service. It proves our algorithm has advantage in dealing a large-scale Web service knowledge model.