Verification Of Web Service Composition Based On An SMT Solver

Web Service has become a new and promising technology in recent years, while the presented concept of services composition makes our life more convenient. Because the process of Web services composition is dynamic, the quality of Web services composition is not guaranteed.Therefore, it is particularly important to verify composit Web service. The common method of verification is Web service composition formal modeling, but most of these methods just consider control-flow based analysis and modeling process is complex, so the verification effect is not ideal.In order to solve the above problem, a method is put forward to verify Web service composition based on an SMT solver. Solving the satisfiability of formula is one of classic NP complete problem and SMT is the problem of deciding the satisfiability of a first order formula with respect to some theory formulas. In addition, it is recognized due to its application value in formal verification and program analysis. The main contributions of this paper are presented as follows:(1) The constraint information is extracted from XML documents provided by composit Web service, so a intermediate file is generated and it includes exection process of Web services compositions, execution conditions of actions in process and definition of variables.(2) After the intermediate file is done further preprocessing that the constraint is classified as variable constraint, assignment constraint, constraint of execution conditions and order constraint,then a constraint document is generated according to the proposed constraint encoding rules. Finally,Web services composition is illustated using Z3 solver.(3) A system of verifying Web services composition is presented based on an SMT solver. The system is added a processing module of verification failure based on the method to verify Web services composition using an SMT solver, that ensures the quality of Web services composition.The method of verification of Web service composition is put forward based on thorough research and it is proved to be feasible through example analysis.