Research On Verification Of Service Composition Based On Probabilistic Model Checking

In the research of QoS-aware Web service composition,the non-functional requirements of the users are the most frequently used criteria for Web service composition.These requirements have uncertain and multi-objective characteristics in the open environments.However,the traditional Web service composition methods can hardly solve these characteristics,they also seldomly consider the impact of dynamic changes of the environment and the dependence among different abstract services.To solve these issuess,we present a series of Web service composition verification methods based on probabilistic model checking.First,we propose a multi-objective verification method based on probabilistic model checking to address the uncertainty and multi-objective characteristic of users' non-functional properties.The Web service composition process is modeled as a quantitative multi-objective Markov decision process.Different user requirements are expressed by multi-objective temporal logic formulas.With the input of the above two models,the optimal solution is found via probabilistic model checking.Second,the QoS of a single Web service under the current environment should be considered when computing the global QoS.To solve this problem,we propose a multi-objective verification method for Web service composition in open environment based on the above multi-objective verification methods.The environment is modeled as a Markov decision process which interacts with the quantitative multi-objective Markov decision process of Web service composition.With the input of the two model and multi-objective temporal logic formulas,the optimal solution can be found via probabilistic model checking.Third,we propose a Web service composition verification method based on the parametric model,which parameterizes the transition probability between different states in the environment model to handle the randomness of the process of environmental changes.Furthermore,the restriction requirements are introduced to constrain the process of Web service composition to model the dependence among abstract services,and alleviate the problem of state explosion during verification.Two examples are delivered to illustrate the proposed methods and the experiment result indicates that these approaches can be used for Web service composition effectively.