Verifying web services of OWL-S with Petri net

The Web service technology is becoming the mainstream for implementing the distributed applications based on architecture oriented service. Simple Web service couldn´t deal with the requirements of complicated distributed system. Some relevant Web services have to be integrated to a composite service to overcome it. Now, more attentions are paid to the quality of service of composite Web service. The OWL-S is an important specification to construct composite Web service for realizing the goals of discovering, composing and executing Web services automatically, but it doesn´t provide the ways to verify its correctness. Petri net is a mature and visual formal method to verifying the distributed systems based on rigid mathematical ground. This paper focuses on verifying the correctness of composite Web services defined by OWL-S. The rules are presented for translating the composite Web service defined by OWL-S into corresponsive Petri Net described by xml style, and a prototype is implemented based on these rules. With an open source Petri net analyzing tool, the correctness and other properties could be verified and analyzed. An example shows that the presented method is feasible.