A formal approach for correct-by-construction system substitution

TL;DR

This paper presents a formal framework using Event-B to ensure correct system substitution, addressing scenarios like adaptation, failure management, and reconfiguration, by providing proof-based correctness guarantees.

Contribution

It introduces a formal approach for verifying the correctness of system substitution using refinement and Event-B, which is novel in ensuring reliable system reconfiguration.

Findings

Formal proof of correctness for system substitution

Application of Event-B to model substitution scenarios

Enhanced reliability in system reconfiguration processes

Abstract

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.