A Model-Driven Engineering Approach for the Formal Verification of Composite Web Services

We propose in this paper a model-driven approach for specifying and verifying Web services composition. In particular, we present how the process engineering and reengineering allows us to check the consistency of Web services composition. To achieve this goal, we based on the Architecture Description Language (ADL) ACME. This ADL is coupled to Armani, a formal language based on first order predicates. Using MDE tools such as ATL, Xtext, Xpand and Check, we have developed a tool WSC2ACME taking as input a textual WSDL specification and outputting the corresponding ACME code. Then, we propose the re-engineering of the process to be able to use it properly, and to ensure the proper functioning of the Web services composition. Our approach aims at improving the existing proposals taking a step forward in simplifying and improving the reliability of service composition.