Model-driven approach supporting formal verification for web service composition protocols

Composite Web services development is a complex task involving specification, verification, implementation, and testing. Despite the fact that several languages have been proposed for composing Web services (e.g., BPEL, WSCI), there is a lack of well-defined formal semantics for formal analysis and verification. Moreover, current approaches are specific to a given programming language (e.g. BPEL) and they focus only on the verification of already implemented composite services. This paper proposes an approach for specifying, verifying and implementing composite services according to the Model-Driven Architecture principles. It makes use of formal methods, especially the LOTOS formal description language, to support composition verification at specification time. The benefit is that the composition specification is proven to be correct before its implementation with a programming language such as BPEL. A case study is also presented to show how a service composition can be specified in a workflow and then formally verified before executable code generation.