SHIP: Formulating the Argument

The safety of system is discussed in the context of the following model.

The diagram shows the standard fault-error-failure model for software. A fault is a defect in the design and is the primary source of the failure. After development, the design could be perfect or faulty. In practice some faults are likely to remain in a complex design after development. However, even if it is faulty, the system may still operate correctly most of the time (i.e. stay in the OK state) until some triggering input condition is encountered. Once triggered, some of the computed values will deviate from the design intent (an error). However the deviation may not be large enough (or persist long enough) to be dangerous, so the system may recover naturally from the "glitch" in subsequent computations ("self healing"). Alternatively explicit design features (e.g. diversity, "firewalls", etc.) can be used to detect such deviations and either recover the correct value (error recovery) or override the value with a safe alternative (fail-safety).

Finally we may simply observe the system as a "black box" where we compute the probability of failure from past experience.

The overall approach to generating the safety case involves:

• characterising the safety case arguments in terms of the transitions of the model
• ensuring the implementation strategy is compatible with the safety argument(s)
• determining and evaluating the evidence to support the claims made about the transition probabilities in the model

For numerical estimates we need to quantify (or at least bound) the transition probabilities on the transition arcs. In a formal argument we claim the transition probability of OK to ERROR is zero. In a probabilistic argument we might combine an error recovery probability (ERROR to OK) with a bounding estimate for the error rate based on operational testing. Alternatively we may simply rely the failure rate observed in the field.

This safety case approach was applied to plant and computer-based examples and appears to be fairly generally applicable.