Research On Verification Of Web Service Based On Abstraction Refinement And Combination Technology

Service oriented architecture (SOA) is a new software development, deployment and integrated model after the object-oriented, component-based development, and provides flexible design and development programs for software development. As a method of SOA, Web services break through the traditional distributed computing model in communication, application range and other constraints. And through the way of services combination, the network application that constructs flexibly and rapidly has penetrated into many of the key industries of national economy.In the existing verification methods of Web services, model checking has been widely used because it has high degree of automation, and can provide a counterexample path. However, because of the large scale of the system, the model checking will cause the state-space explosion problem in the process, how to select the suitable way to relieve state-space explosion has become a research hot spot in service verification field. In this dissertation, by introducing predicate abstraction and refinement techniques into the traditional model checking method, we propose an abstraction refinement verification framework for Web services, to verify the security of the internal process logic and the compatibility between services.Major work and contributions of this dissertation are as follows: First, we Use Kripke structure to construct the model for Web service, and gain predicate formula collection through disintegrating properties into atom proposition, then compose the abstract Kripke structure using predicate abstract techniques, and finally combine all abstract models to get the combined abstract model of verification system. Second, we propose the rule of conversion abstract Kripke structure to Promela language, then verify the properties with the Spin model checker, if not satisfied, the counterexample is given. The counterexample will be confirmed by doing projection operation in the Web services. Then refine the abstract model of Web service which causes spurious counterexample, and generate a new combination of the abstract models to verify the properties again. Third, based on the above two aspects, we propose an abstraction refinement verification framework for Web services, and illustrate the feasibility of the approach in remission of the state space explosion problem.