Model transformation and formal verification for Semantic Web Services composition

Web services composition is becoming more and more important in today’s service oriented business environment. We need to compose services from different providers together to fulfill the business goals that cannot be satisfied by any single service. However, different services often have semantic inconsistencies which may lead to the failure of the services composition. In order to verify the correctness of the Semantic Web Services composition, this paper proposed a composition model of Coloured Petri Nets which is transformed from OWL-S model. This model can express the logical relations among the sub-processes of the services composition explicitly, and verify the correctness of the services composition using formalized methods of Coloured Petri Nets. This paper presented the verification algorithms for the reachability, boundness and semantic consistency of composed services. Furthermore, an example of collaborating design process was given to simulate and execute the model.