Abstract
In the effort to develop critical systems, taking account of failure modes is of vital importance. However, when systems fail (even in a manner previously determined as acceptable), a lot of the invariants that hold in the case of nominal behaviour also fail. A technique is proposed that permits the inclusion
of the strong invariants of nominal behaviour alongside the provisions for degraded behaviour in an inclusive formal system model. The faulty system model is derived from the nominal one via fault injection, and the nominal and faulty system models are related via a formal retrenchment step. Manipulation of the retrenchment data permits the inclusion of the stronger invariants, which remain provable when faults are disabled in a generic manner in the faulty model, thus increasing confidence in the overall system design. The details are developed in Event-B, and the concept is illustrated using a toy switching example.
of the strong invariants of nominal behaviour alongside the provisions for degraded behaviour in an inclusive formal system model. The faulty system model is derived from the nominal one via fault injection, and the nominal and faulty system models are related via a formal retrenchment step. Manipulation of the retrenchment data permits the inclusion of the stronger invariants, which remain provable when faults are disabled in a generic manner in the faulty model, thus increasing confidence in the overall system design. The details are developed in Event-B, and the concept is illustrated using a toy switching example.
| Original language | English |
|---|---|
| Title of host publication | The 5th International Symposium on Model-Based Safety and Assessment (IMBSA 2017) |
| DOIs | |
| Publication status | Published - 2017 |