Study Of Web Service Composition Based On Petri Nets

As the corner stone technology of Service Oriented Architecture (SOA), Web service has widely been adopted in academic and industry communities. The popularity of Web service technology also turned the Software-as-a-Service (SaaS) design theory into a practical system architecture paradigm. With Web services, new functions can be easily built by composing existing Web services. Currently, automatic Web services composition and verification are key challenges in the Web services research. In this paper, we investigate the two aspects based on Petri-net theories.1. An extended model checking method based on colored Petri nets is proposed. Based on local model checking algorithm of CTL (Computational Tree Logic) in colored Petri nets, an algorithm for searching witness or counterexample of the model checking result is investigated. The algorithm is implemented using ML (Metal Language) language, and fluently integrated in the colored Petri net model checking tool named CPN-tools. Then, the extended CPN model checking tool can be used in the verification of Web services composition. The method can not only check the logical errors in some systems, but also tell users the reasons for the errors. This extension provides the technical guarantees for the Web services composition validation based on the colored Petri nets. Our experiments demonstrate that the extension is correct and effective.2. This paper proposes a colored Petri net based approach for the modeling, simulation and verification of the Web service compositions based on orchestrations or choreographies. First, the mapping rules from BPEL and WSCI to colored Petri nets are introduced; then CTL based colored Petri nets model checking approach is applied to verify Web service compositions for error detection. Our experiments demonstrate the Web service verification based on colored Petri nets is more practical, reliable and effective.3. This paper proposes a new backward reasoning algorithm based on algebra. The algorithm fully takes advantage of mathematics foundation of Petri nets, is of parallel computing capability and simpler data structure. The method is much easier for implementation. In addition, based on the backward reasoning method, a complex system can be transformed into a simpler system closely related to the current problems. Thus, the space complexity of the algorithm can be reduced. The feasibility was testified through practice. This algorithm provides the technical support for evaluating the semantic matchmaking degree of dynamic Web services composition.4. An automatic Web services composition based on Petri nets is presented. With this method, we first obtain a Petri net model that represents the data dependent relationship between the service composition according to consumers' demands and the current available services. Then, plans of the service composition are obtained. Further, Fuzzy Petri net (FPN) is utilized to evaluate the semantic matching degree of each kind of combination plan, and the generalized stochastic Petri net (GSPN) is employed to analyze the performance of the plan with better semantic matching degree. Then, a better performance composition plans can be obtained on the basis of guaranteeing high success ratio of composition. Finally, one can pick out the better plan and transform it into an operational code framework in BPEL. Compared with other approaches available, our method takes full advantages of Petri nets, such as easy description, analysis and evaluation of the systems, to obtain a better plan of Web service compositions.