A Verification Of Web Services Compositions Based On Model Checking Multi-agent Systems And Abstraction

As the rising of service-oriented architecture, web service is the trend ofservice and software development. In most situations, single web servicescannot satisfy users’ complex requirements, because of their single functions.A technology integrates multiple web services according to particularcompositions, and provides a unique interface to users with different demandsto access the services. However, Credibility of services, comprisingcorrectness, reliability, security, usability, and timeliness, is challenged bydynamics of services and cooperations, by open and volatile operatingenvironment of the internet, and by the nondeterminacy of servicesdevelopment and of services running caused by the loosely couplingdevelopment mode. To guarantee the credibility, researchers keep trying toverify specifications of services and compositions.Formal method is the main verification. Relative to ordinary formalmethods, model checking works completely automatically, and returnscounterexamples and witnesses for verified formulas. Another advantage ofmodel checking is that, it determines the truth of formulas in the verifiedmodel instead of in the whole domain of the modal logic. Among verificationtechniques on the base of model checking, verifying based on model checkingmulti-agent systems performs better, because it verifies not only CTLspecifications, LTL specifications, but also CTL*specifications, evenepistemic specifications. State explosion problem remains the main problemof model checking. As a solution, abstracting attracts many researchers,resulting the constant rising of many achievements.In this paper, a graph-like counterexample-guide abstract and refinementfor symbolic model checking multi-agent systems is raised, based on which,we provide a methodology of verification of web services compositions. Themain contribution of the methodology is the reduction of state explosion problem encountered by verifying web services compositions based on modelchecking multi-agent systems. Another contribution is that, we solve theproblem of abstract for symbolic model checking multi-agent systems whichis not solved by previous counterexample-guided abstract for model checkingordinary systems, and that the Kripke structure adopted in this paper is moreformal than the model adopted in previous work. The correctness of themethodology is proved theoretically and the effectness is shown by theexperiment. The main work of this thesis can be summarized as follows:(1) An abstract model of Kripke structure of multi-agent systems with aproof of property preservation theorem; an approximating approach, resultingin an approximation of abstract system, with a proof of its satisfaction ofproperty preservation theorem.(2) A kind of graph-like counterexample for model checking multi-agentsystems, with a formal proof and a generation.(3) A graph-like counterexample-guided abstract and refine technique forsymbolic model checking multi-agent systems.(4) A performance of the previous transformation from the BPEL describedbusiness processes of web services compositions to SMV describedmulti-agent systems, after the comparation among specifications of webservices compositions and the verification.(5) A methodology for verification of web services compositions based onmodel checking multi-agent systems and the graph-likecounterexample-guided abstract and refine.