Premium
Formal verification of safety‐critical systems
Author(s) -
Moser Louise E.,
MelliarSmith P. M.
Publication year - 1990
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/spe.4380200804
Subject(s) - computer science , consistency (knowledge bases) , formal methods , formal verification , life critical system , abstraction , reliability engineering , software verification , formal specification , software , software system , software engineering , programming language , engineering , software construction , philosophy , epistemology , artificial intelligence
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.