Extension of Model Checking Tool of Colored Petri Nets and Its Applications in Web Service Composition

Formal description and verification of Web services composition are important research issues. To better complete the verification, an extended model checking method based on colored Petri nets is proposed. The latest version of the colored Petri net model checking tool can only determine the correctness of temporal logic formulas, and no further diagnosis information is available. Based on the 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(meta 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 service composition. With this approach, CPN is used to describe the behaviors of Web service composition, and CTL logic formulas are used for specifying the requirements of target Web services. The method can not only check the logical errors in Web service composition, but also tell users the reasons for the errors. This extension provides the technical guarantees for the Web service composition validation based on the colored Petri nets. Experiments demonstrate that the extension is correct and effective.