Modeling and Formal Verification of Web Services Composition Using CADP

A growing number of companies are using web services to make their expertise and data available through the network. The current problem is the integration of these services with the aim of implementing business-to-business (B2B) collaboration. This task of collaboration is called the composition of web services. The main objective of this research work is proposing a new approach of modeling and verifying web services composition. This approach allows a clear and structured modeling and easy verification regardless of the number of services to be composed and the degree of complexity of composition. Concerning the contribution, we firstly propose a modeling of the composed system based on the multi agent systems and precisely the Multi-agent reactive decisional system (MARDS), and using the BPM (Business Process Management) standards in particular the BPMN notation. Secondly, we seek to verify this modeling to prove its correctness before implementing it. For verification, we propose a transformation of the BPMN model to a formal LOTOS specification, which has the advantage of being supported by formal verification tools such as the CADP toolkit, which allows to apply the behavioral properties and validate the system of Web services composition