Distributed Reconfigurable B approach for the specification and verification of B-based distributed reconfigurable control systems

This research article proposes a novel approach called Distributed Reconfigurable B to specify and verify distributed reconfigurable control systems using B method. Reconfiguration signifies the dynamic adaptation of the system behavior to the evolution of its environment by applying a reconfiguration scenario. A multi-agent architecture is defined to affect a reconfiguration agent to ensure local reconfiguration for each subsystem and a coordination agent to manage the different subsystems to guarantee the coherence of the whole system. A reconfigurable system is a set of B operations where only a subset is executed by adding or removing operations after a well-defined reconfiguration scenario. Distributed Reconfigurable B defines two complementary steps to be applied in abstract model of B method: specification and verification. The first step models the agents according to Distributed Reconfigurable B formalism. The second verifies distributed reconfigurable control systems using Atelier B tool and avoids the redundant checking of different B machines by applying the implemented Check Reconfigurable B tool. We apply the contributions on the two benchmark production systems: FESTO and EnAS.