Hierarchical Colored Petri Nets Based Modeling And Verification For Dynamic Web Service Composition

With the development of web services technology, more and more web services have been published on the internet. When an individual service can not meet the needs of users, it is necessary to compose several function limited services, so that it can produce value-added services. Manual combination of Web service can not dynamically adjust web services composition process according to the changes of user needs, so there is an urgent need for a dynamic combination of these Web services. Web services processes described by web ontology language OWL-S can make web services include machine understandable semantic information, thus it can lead web services to realize the automatic discovery, composition, execution and monitoring. But the dynamic web services composition is a complex and error-prone process. For lacking of effective verification mechanism, it is necessary to establish formal description model of web services composition, and through the analysis and verification of models to verify the correctness and effectiveness of dynamic web services composition.There are already formal verification methods have been proposed, mainly based on process algebra, automata and Petri nets. But the process algebra and automata methods are only in the syntax level, they have not enough semantic description for Web service, also they have complex modeling process, and the abstract models lack of intuitive graphical representation. Because basic Petri nets without color and hierarchical concept, so the method can not express different types of data of web services accurately, and for large-scale and complex systems, it is easy to lead state space explosion problem.In this paper, based on the semantics of web services ontology language OWL-S, a modeling and verification method using Hierarchical Colored Petri nets (HCPN) for web services composition processes is proposed. First of all it researches the semantic Web service dynamic composition process based on OWL-S, and get Web service composition model. Then the transformation rules from Web service composition process described by OWL-S to CPN model are proposed. The atomic processes, composite processes and the control structure were mapped to CPN model with the same semantic structure, and then get the corresponding HCPN model of Web service dynamic composition process. Finally with the help of CPN-Tools, the established HCPN model can be simulated dynamicly, the dynamic behaviors of the model such as boundedness, accessibility, activity (whether the deadlock can be detected) can be verified through the state space mechanism, and the correctness and effectiveness of web services composition can be verified.Hierarchical colored Petri nets (HCPN) based modeling method make up the shortage of basic Petri nets, it introduces the token with different colors and changed number to represent the IOPE of the OWL-S model, the control flow and data flow of Web services can be characterized better. The introduction of hierarchical concept, which can simplify the model, for large-scale and complex systems, it can be divided into several subnets, give an independent verification for each stage, step refinement. If some subnets have same structure, there is no need to repeat the modeling process, also it help to avoid state space explosion problem.