Research On Model Checking Based On Conditional Transition And Its Application In Web Service Verification

Web service is a service oriented computing application.Different developers use different logic control flows combine heterogeneous and multi-platform Web services to a new Web service and we call it Web composite service.It is difficult to guarantee the safety of Web composite service control flow.The purpose of the thesis is to solve the safety of Web composite service control flow.In this thesis,we consider the Web composite service as a multi-agent system,and use the conditional transition based model checking method verify Web composite service.The model checking method is based on building conditional transition system.The model checking method based on conditional transition is divided into dynamic model checking method which is based on dynamic modeling method and static model checking method which is based on static modeling method.The core idea of conditional transition based model checking method is to generate the state set and transition relationship set of the system according to rule set.The dynamic model checking method has a good advantage in modeling efficiency and error location efficiency.In this thesis,the dynamic model checking method is used to verify Web composite service.State explosion is a problem that always exists in the process of model checking.For large-scale Web composite service,the state explosion problem still exists.The thesis uses conditional transition model checking method based on external memory to solve the problem.The thesis combines the idea of breadth-first searching algorithm and the idea based on external memory and proposes conditional transition model checking algorithm based on external memory.The algorithm uses the idea of conditional transition based model checking method and uses the method of the block operation handle a new generation of a large number of states.The method can relieve the pressure of memory and makes it possible for the model detector to verify a large scale system.In this thesis,we present the rule set of Web composite service and the conditional transition system of Web composite service according to the rule set,and we also analysis the counterexample paths of Web composite service.The thesis improves the model detector NuSMV and uses improved model detector verify Web composition service.Then we compare with other model detectors(Spin,NuSMV,etc.)by using experiment,and come to conclusion that the model checking method based on conditional transition has the ability to verify the safety of bigger Web composite service.