Formal verification in Web services composition

The aim of this research is to propose a method for verifying business processes automatically generated through Web services composition. The method is based on model checking and uses Spin model checker, a tool for verifying the correctness of software models. Model checking is a powerful verification technique that can be applied to hardware or software systems in order to validate safety requirements such as the absence of deadlocks. The business process is transformed into a PROMELA model that is simulated by Spin in order to be verified against the constraint requirements specified. The proposed method is incorporated into a generic and extensible framework for automatic Web services composition and execution.