Event-B Formalisation of Web Services for Dynamic Composition

The capacity of a composite service to change configuration according to the component services behavior is essential. In particular, this reconfiguration should be done dynamically without disturbing the service execution. To the best of our knowledge, few works were interested in verifying the coherence of this dynamic reconfiguration. By dynamic reconfiguration we mean for example, overcome the failure or the unavailability of a service component by the the discovery and the replacement of another service that provides the same functionalities. But, the new service may have the same structure but provide additional features that can make the composite service not behaving as expected. To do so, we propose an approach based on Event-B for a formal verification of the structural and behavioral properties of the component service before dynamically integrated into the composition during the execution.