Describing and Verifying Semantic Web Service Composition with MDA

Describing and verifying OWL-S with the Unified Modeling Language (UML) cannot only improve the efficiency of developing semantic Web service, but also ensure the correctness of dynamic composition process; abstractly modeling semantic Web services with model-driven architecture (MDA) at a higher level is helpful for dynamically binding services. This paper proposes an effective approach to describe and compose semantic Web service with UML, a verification mechanism is imported to ensure the correctness of semantic Web service composition; class diagrams and use-case diagrams are used to model the static aspect of OWL-S, activity diagrams to model the behavior of an OWL-S composition process. In this paper, the transformation from UML models of semantic Web service composition to the model-checking language Promela was presented for verifying the correctness of Web service composition using automated verification tool SPIN.