Safety requirements and fault trees using retrenchment

Abstract

In the formal modelling of safety critical systems, an initial abstract model captures the ideal, fault free, conception of the system. Subsequently, this model is enriched with the detail required to deal with envisaged faults that the system is designed to be robust against, resulting in a concrete extended system model. Normally, conventional refinement cannot provide a formal account of the relationship between the two models. Retrenchment, a liberalisation of refinement introduced to address such situations, allows model evolution, and is deployed to provide a formal account of the fault injection process that yields the extended system model. The simulation relationship of retrenchment is used to derive fault trees for the faults introduced during the injection process. A two bit adder example drawn from the FSAP/NuSMV-SA safety analysis platform is used to illustrate the technique. © Springer-Verlag 2004.