Formal verification of flight critical software

Steven P. Miller, Elise A. Anderson, Lucas G. Wagner, Michael W Whalen, Mats Heimdahl

Research output: Chapter in Book/Report/Conference proceedingConference contribution

28 Scopus citations


Recent advances in modeling languages have made it feasible to formally specify and analyze the behavior of large system components. Synchronous data flow languages, such as Lustre, SCR, and RSML-e are well suited to this task, and commercial versions of these tools such as SCADE and Simulink are growing rapidly in popularity among designers of safety critical systems, largely due to their ability to automatically generate code from the models. At the same time, advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle. This report describes how such formal verification tools have been applied to the FCS 5000, a new family of Flight Control Systems being developed by Rockwell Collins Inc.

Original languageEnglish (US)
Title of host publicationCollection of Technical Papers - AIAA Guidance, Navigation, and Control Conference 2005
Number of pages16
StatePublished - Dec 1 2005
EventAIAA Guidance, Navigation, and Control Conference 2005 - San Francisco, CA, United States
Duration: Aug 15 2005Aug 18 2005

Publication series

NameCollection of Technical Papers - AIAA Guidance, Navigation, and Control Conference


ConferenceAIAA Guidance, Navigation, and Control Conference 2005
Country/TerritoryUnited States
CitySan Francisco, CA


Dive into the research topics of 'Formal verification of flight critical software'. Together they form a unique fingerprint.

Cite this