Skip to content

Software Quality

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 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 proves their absence over every execution by sound over-approximation (Astrée on Airbus flight-control code); theorem proving carries the strongest guarantee where the effort is justified (the seL4 kernel, the CompCert compiler); bounded model checking proves it up to a depth on C/C++ and register-transfer-level (RTL) designs.
  • Safety properties that must hold over time. Model checking proves safety and liveness properties written in temporal logic against a model, and temporal-logic falsification 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 bounds the worst-case execution time so a task is provably schedulable.
  • Fault tolerance. Fault injection corrupts registers and memory (software-implemented fault injection) to test survival of transient hardware faults, and probabilistic model checking 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 generates scenarios, runs them in simulation, and checks them against safety envelopes such as Responsibility-Sensitive Safety.
  • Structural coverage as certification evidence. Exhaustive coverage — 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)1; road vehicles scale by Automotive Safety Integrity Level under ISO 26262 (ISO 2018)2; general electrical and electronic systems scale by Safety Integrity Level under IEC 61508 (IEC 2010)3; medical-device software scales by safety class under IEC 62304 (IEC 2006)4. 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)5, 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)6.

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

References

  1. RTCA. 2011a. DO-178C: Software Considerations in Airborne Systems and Equipment Certification. https://www.rtca.org/do-178/. ↩

  2. ISO. 2018. ISO 26262: Road Vehicles — Functional Safety. International Organization for Standardization. https://www.iso.org/standard/68383.html. ↩

  3. IEC. 2010. IEC 61508: Functional Safety of Electrical/Electronic/Programmable Electronic Safety-related Systems. https://webstore.iec.ch/en/publication/5515. ↩

  4. IEC. 2006. IEC 62304: Medical Device Software — Software Life Cycle Processes. https://webstore.iec.ch/en/publication/6792. ↩

  5. ISO. 2022. ISO 21448: Road Vehicles — Safety of the Intended Functionality (SOTIF). International Organization for Standardization. https://www.iso.org/standard/77490.html. ↩

  6. Underwriters Laboratories. 2023. ANSI/UL 4600: Standard for Safety for the Evaluation of Autonomous Products. Underwriters Laboratories. https://www.shopulstandards.com/ProductDetail.aspx?productid=UL4600. ↩