Formal verification of safety‐critical systems
Louise E. Moser, Peter Michael Melliar-Smith · Software Practice and Experience · 1990
Abstract We describe our practical experience in the use of formal verification to obtain increased confidence in the design of safety‐critical systems. The experiment involved demonstrating the consistency of the design specifications of SIFT, a software‐implemented fault‐tolerant operating system for aircraft flight control. Specifications were written at successive levels of abstraction from the most abstract requirements definition down to the detailed level of program code. Consistency of the successive levels of specification was demonstrated using the enhanced HDM verification system. Formal verification is currently feasible only for carefully simplified systems, but there appears to be no alternative method that can meet the extreme safety requirements for safety‐critical systems.