The Analysis And Verification Of Web Service Composition Based On Petri Nets

Web Service is a self-describing, self-contained and available network module that performs specific business function,interpreting the concept of "a software as a service". The environment of Web services composition is dynamic, heterogeneous, widely distributed.It also involves collaboration and interaction among multiple autonomous organizations. Hence the importance of verifying the quality of Web services composition methods is becoming increasingly significant.Petri nets not only simulate the operation of a system, but also describe the structural properties of the system. So Petri nets dynamically reflect the actual operation of a complex system. Therefore,we use Petri nets to validate the quality of Web services composition.The main work of this paper includes:(1) we use Tools4 BPEL to generate a Petri net model of a BPEL file;(2) we use the rules of Petri net reduction to simplify the Petri net model;(3) we use the Petri net algorithm to simplify the reachable state graph;(4) we analyze and verify the reachable state graph;(5) we propose an optimization algorithm of Petri net to optimize the reachable state graph.The main contributions of this paper are listed as follows:(1) Integrate Petri net reduction rules and the reachable state graph.We use the reduced graph to analyze the important properties of Petri nets. The reduced graph of a complex Petri net model can improve the efficiency of the analysis.Then we use tools to verify the analysis results.The result shows that the analysis method is right and feasible.(2) Propose Petri net optimization methods.According to Petri net theorems and inferences,we use the optimization method to optimize the reachable state graph. Then we analyze the optimized reachable state graph by the theorems and inferences.The experiment has proved that the optimization method is right and feasible.