Modeling and Verification of B-based Distributed Reconfigurable Control Systems

The paper deals with the modeling and verification of B based Distributed Reconfigurable Control Systems (DRCS). A distributed multi-agent architecture is developed, where for each system is affected a Reconfiguration Agent to apply a local automatic reconfiguration, and a Coordination Agent is proposed to harmonize between systems when any local reconfiguration is applied in a system. We apply the Distributed Reconfigurable B "DR-B" formalism to define all possible behaviors, to determine reconfiguration functions for each system and to execute the appropriate ones to respond to reconfiguration requests and to switch between the specific distributed configuration at run-time to cope with the coherence of running systems. We verify a DRCS by using the B method. The goal is to guarantee the consistency and the correctness of the abstract specification level. Further more, to avoid combinatorial explosion problem in DRCS, we apply the "Check RB" tool, to reduce redundant checking of different behaviors sharing similar operations. All the contributions of this work are applied to two benchmark production systems FESTO and EnAS.