A formal approach for correct-by-construction system substitution
This work addresses system reliability in scenarios like adaptation or failure management, but it appears incremental as it builds on existing formal methods without introducing a new paradigm.
The paper tackles the problem of ensuring correctness when substituting one system for another, proposing a formal approach using refinement and the Event-B method to prove correctness.
The substitution of a system with another one may occur in several situations like system adaptation, system failure management, system resilience, system reconfiguration, etc. It consists in replacing a running system by another one when given conditions hold. This contribution summarizes our proposal to define a formal setting for proving the correctness of system substitution. It relies on refinement and on the Event-B method.