A System Substitution Mechanism for Hybrid Systems in Event-B

Changes like failure or loss of QoS are key aspects of hybrid systems that must be handled during their design. Preserving the system state is a common requirement that can be ensured by reconfiguration relying on system substitution. The specification and design of these systems usually rely on continuous functions whereas their implementation is discrete. Moreover, the associated safety properties are characterized by a safety envelope defining safe system states. This paper presents a novel approach for formalizing the system substitution mechanism for hybrid systems, in which the system substitution maintains a safety envelope of the given hybrid system during system failure or switching from one supporting system to another. Proving the correctness of the discrete implementation of the defined reconfiguration mechanism for hybrid systems is a challenging problem. In this purpose, we propose to combine system substitution and incremental system modeling to ensure correct discretization. We rely on the Event-B method and the Rodin Platform with the Theory plug-in to develop the system models and carry out the proofs on dense real numbers.