Modeling and Verifying Composite Semantic Web Service Based on Colored Petri Nets

In this paper, colored Petri nets are used to model the atomic processes and the composite processes of semantic Web services. After introducing the concept about the colored Petri net and the knowledge associated with OWL-S, colored Petri nets are used to model the composite processes of semantic Web services. In this model, input, output and precondition are represented through different kinds of tokens, effect is represented by the change of the token number during firing the transition, the composition model can be described unambiguously and the composite process can be analyzed and verified conveniently. Then, an algorithm is given to verify the model syntax correctness. Finally, the composite service model is applied to a case.