A General Framework for Automatic Verification of Web Services

Efficient integration of business processes goes a long way in achieving a complete self managing system. Web services related developments provide the technology for building complex distributed systems focusing on the efficient integration of the involved processes. The interaction details and behavior of processes in distributed systems are specified, in this context, by the constructs provided by Web services specification languages. Formally verifying such specifications is a complex task, as the specifications cannot be easily verified by standard formal verification tools. This work developed a framework for automated verification of Web services which use semantic markup languages like, OWL-S for their description, composition and integration. Here we describe a method devised to translate process model description in OWL-S into its equivalent process description in Promela so as to verify the same using the SPIN Model Checker.