# Verifying safety-critical systems

A **safety-critical** system is one whose failure can cause physical harm: an
aircraft flight controller, an anti-lock brake, an infusion pump, a rail
interlocking. Safety here means freedom from unacceptable risk of harm, judged
against a hazard or a safety envelope rather than only a functional spec. The
work runs in three parts: identify the hazards, verify that the system avoids
them, and argue the case at a rigor scaled to the risk. Safety is not a separate
quality dimension; it folds into Functionality (hazard-avoidance verified to an
assurance level) and Reliability.

## Identifying hazards

Before any code is verified, [safety analysis](https://quality.stereobooster.com/safety-analysis.md) enumerates
what can go wrong and how a failure propagates to harm. Its output is the set of
hazards and safety requirements that everything downstream is verified against.

## Verifying the system stays safe

The verification methods sort by what each one establishes about a hazard.

- **Absence of runtime errors** that could trigger a hazard, such as overflow,
  out-of-bounds access, or division by zero. [Abstract
  interpretation](https://quality.stereobooster.com/abstract-interpretation.md) proves their absence
  over every execution by sound over-approximation (Astrée on Airbus
  flight-control code); [theorem proving](https://quality.stereobooster.com/theorem-proving.md)
  carries the strongest guarantee where the effort is justified (the seL4
  kernel, the CompCert compiler); [bounded model
  checking](https://quality.stereobooster.com/bounded-model-checking.md) proves it up to a depth on
  C/C++ and register-transfer-level (RTL) designs.
- **Safety properties that must hold over time.** [Model
  checking](https://quality.stereobooster.com/model-checking.md) proves safety and liveness
  properties written in temporal logic against a model, and [temporal-logic
  falsification](https://quality.stereobooster.com/temporal-logic-falsification.md) searches for an input
  signal that drives the real system outside a signal-temporal-logic envelope.
- **Timing.** In hard-real-time systems a missed deadline is itself a hazard;
  [WCET analysis](https://quality.stereobooster.com/wcet-analysis.md) bounds the worst-case execution
  time so a task is provably schedulable.
- **Fault tolerance.** [Fault injection](https://quality.stereobooster.com/fault-injection.md)
  corrupts registers and memory (software-implemented fault injection) to test
  survival of transient hardware faults, and [probabilistic model
  checking](https://quality.stereobooster.com/probabilistic-model-checking.md) computes failure
  probabilities over dynamic fault trees.
- **The operating space of cyber-physical and autonomous systems.** The hazard
  lives in the physical scenarios the system meets rather than in the code
  alone. [Testing autonomous systems](https://quality.stereobooster.com/testing-autonomous-systems.md)
  generates scenarios, runs them in simulation, and checks them against safety
  envelopes such as Responsibility-Sensitive Safety.
- **Structural coverage as certification evidence.** [Exhaustive
  coverage](https://quality.stereobooster.com/exhaustive-coverage.md) — MC/DC (modified
  condition/decision coverage) and multiple-condition coverage — is a bounded
  proof over a decision's logic, and the highest assurance levels mandate it as
  evidence that testing exercised the code.

## Assurance: rigor scaled to risk

No system is verified to an absolute standard; the functional-safety regimes fix
how much verification a component needs by the severity of the hazard it can
cause. Avionics software scales its objectives by Design Assurance Level under
DO-178C (RTCA 2011a)[^do178c]; road vehicles scale by Automotive Safety Integrity Level
under ISO 26262 (ISO 2018)[^iso26262]; general electrical and electronic systems scale by
Safety Integrity Level under IEC 61508 (IEC 2010)[^iec61508]; medical-device software
scales by safety class under IEC 62304 (IEC 2006)[^iec62304]. Two newer standards address
gaps the classic regimes leave: ISO 21448 covers safety of the intended
functionality (SOTIF), where the hazard arises from intended-but-insufficient
behavior rather than from a fault (ISO 2022)[^iso21448], and the goal-based UL 4600 frames
the whole assurance effort as a **safety case**, a structured and
evidence-backed argument that the system is acceptably safe for its context
(Underwriters Laboratories 2023)[^ul4600].

## Reading the guarantee

The methods differ in what a passing result licenses. Sound static analysis and
machine-checked proof are *exhaustive* or *mathematical*: they establish that a
hazard class cannot occur. Model checking is exhaustive over a *finite model*.
Falsification, autonomous-scenario testing, and fault injection are *empirical*:
they find envelope violations but cannot prove their absence. A safety case
therefore weights methods to the hazard, leaning on proof and sound analysis
where a failure is catastrophic and on testing where the space is too large to
close.

## Referenced by

- [Security](https://quality.stereobooster.com/security.md) · Quality dimensions
- [Safety analysis](https://quality.stereobooster.com/safety-analysis.md) · Methods

## References

[^do178c]: RTCA. 2011a. *[DO-178C: Software Considerations in Airborne Systems and Equipment Certification](https://www.rtca.org/do-178/)*. <https://www.rtca.org/do-178/>.
[^iso26262]: ISO. 2018. *[ISO 26262: Road Vehicles — Functional Safety](https://www.iso.org/standard/68383.html)*. International Organization for Standardization. <https://www.iso.org/standard/68383.html>.
[^iec61508]: IEC. 2010. *[IEC 61508: Functional Safety of Electrical/Electronic/Programmable Electronic Safety-related Systems](https://webstore.iec.ch/en/publication/5515)*. <https://webstore.iec.ch/en/publication/5515>.
[^iec62304]: IEC. 2006. *[IEC 62304: Medical Device Software — Software Life Cycle Processes](https://webstore.iec.ch/en/publication/6792)*. <https://webstore.iec.ch/en/publication/6792>.
[^iso21448]: ISO. 2022. *[ISO 21448: Road Vehicles — Safety of the Intended Functionality (SOTIF)](https://www.iso.org/standard/77490.html)*. International Organization for Standardization. <https://www.iso.org/standard/77490.html>.
[^ul4600]: Underwriters Laboratories. 2023. *[ANSI/UL 4600: Standard for Safety for the Evaluation of Autonomous Products](https://www.shopulstandards.com/ProductDetail.aspx?productid=UL4600)*. Underwriters Laboratories. <https://www.shopulstandards.com/ProductDetail.aspx?productid=UL4600>.

## Acronyms

- MC/DC — modified condition/decision coverage
- RTL — register-transfer level
- SOTIF — safety of the intended functionality
- WCET — worst-case execution time