Event-B formalisation for dynamic composition: A logistics-based process as a use case

Abstract

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 discovery and the replacement of another service that provides the same functionalities. 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. A logistics-based process is used as use case in order to validate our approach. © 2013 Springer-Verlag Berlin Heidelberg.