Formal Methods

Formal Verification of Safety-Critical Software (Powerpoint)

Almost all of the capabilities developed in this project depend on the use of formal verification tools such as model checkers and theorem provers. Model checkers use a variety of underlying technologies, but essentially work by checking if a property holds for every reachable state. Recent breakthroughs have made it possible for symbolic (BDD-based) model checkers to explore very large (10²⁰ to 10²⁰⁰) reachable states. Bounded model checkers use a combination of state space exploration and induction to deal with even larger state spaces.

Theorem proving is a technique where both the system and its desired properties are expressed as formulas in a mathematical logic, and these properties are shown to hold through use of a mechanical theorem prover. While theorem provers do not have the state space limitation of model checkers, they generally require more skill and labor to prove the desired properties.

As part of this project, we have developed translators from several modeling languages to a variety of model checkers and theorem provers. In the first part of the project, we demonstrated the viability of this approach by developing translators from the RSML^-e language to the NuSMV model checker and the PVS theorem prover. Using these translators, we were able to prove hundreds of functional and safety properties about the mode logic of a Flight Guidance System, finding several errors in the process. More details can be found in the papers listed at the end of this page.

To make this same capability available with commercial tools, we recently developed translators from the Lustre language that the SCADE tool set from Esterel Technologies is based on, making it possible to prove properties about SCADE models. By using the Simulink gateway provided by Esterel Technologies, we have also been able to prove properties of Simulink models.

Most recently, we have developed a translator from Lustre to the SAL (Symbolic Analysis Language) developed by SRI International, allowing us to use the model checkers and theorem provers included in the SAL toolset. We have also developed translators from the Reactis test case generation tool to Lustre, providing an alternative path from Simulink to Lustre. This translator is being extended to support a subset of StateFlow models as well as Simulink.

Publications Related to Formal Methods

• Michael W. Whalen, John D. Innis, Steven P. Miller, and Lucas G. Wagner, ADGS-2100 Adaptive Display & Guidance System Window Manager Analysis, NASA Contractor Report, November 2005.
• Anjali Joshi, Mats P.E. Heimdahl, Steven P. Miller, and Mike W. Whalen, Model-Based Safety Analysis, NASA Contractor Report, November 2005.
• Anjali Joshi, Steven P. Miller, Michael Whalen, and Mats P.E. Heimdahl, A Proposal For Model-Based Safety Analysis, in Proceedings of the 24th Digital Avionics Systems Conference (DASC'05), Washington, D.C., October 30-November 3, 2005. Selected as best paper of the Open Systems Architecture track.
• Steven P. Miller, Mike W. Whalen, Dan O’Brien, Mats P.E. Heimdahl, and Anjali Joshi, A Methodology for the Design and Verification of Globally Asynchronous/Locally Synchronous Architectures, NASA Contractor Report NASA/CR-2005-213912, Sept. 2005.
• Steven P. Miller, Elise A. Anderson, Lucas G. Wagner, Michael W. Whalen, and Mats P.E. Heimdahl, Formal Verification of Flight Critical Software, in Proceedings of the AIAA Guidance, Navigation and Control Conference and Exhibit, San Francisco, August 15-18, 2005.
• Steven P. Miller, Early Validation of Requirements, in Proceedings of the World Computer Congress 2004, Toulouse, France, August 23-27, 2004.
• Alan C. Tribble, Steven P. Miller and David L. Lempia, Software Safety Analysis of a Flight Guidance System , NASA/CR-2004-213004, March 2004.
• Steven P. Miller, Alan C. Tribble, Michael W. Whalen, and Mats P. E. Heimdahl, Proving the Shalls: Early Validation of Requirements Through Formal Methods, Journal of Software Tools for Technology Transfer, [in press].
• Alan C. Tribble and Steven P. Miller, Safety Analysis of Software Intensive Systems, IEEE Aerospace and Electronic Systems, Vol. 19, No. 10, pp. 21 - 26, October 2004.
• Alan C. Tribble and Steven P. Miller, Software Safety Analysis of a Flight Management System Vertical Management Function - A Status Report, Proceedings of the 22nd Digital Avionics Systems Conference (DASC'03), October 2003.
• Anjali Johsi, Steven P. Miller, and Mats P. E. Heimdahl, Mode Confusion Analysis of a Flight Guidance System Using Formal Methods, in Proceedings of the 22^nd Digital Avionics Systems Conference (DASC’03), Indianapolis, Indiana, Oct. 12-16, 2003. Selected as best paper of the Intelligent Interactive Systems-1 session.
• Steven P. Miller, Mats P.E. Heimdahl, and Alan C. Tribble, Proving the Shalls, in Proceedings of FM 2003: the 12^th International FME Symposium, Sept. 8-14, 2003
• Steven P. Miller, Alan C. Tribble, Timothy M. Carlson and Eric J. Danielson, Flight Guidance System Requirements Specification , NASA/CR-2003-212426, June 2003.
• Alan C. Tribble, David D. Lempia, and Steven P. Miller, Software Safety Analysis of a Flight Guidance System, in Proceedings of the 21st Digital Avionics Systems Conference (DASC'02), Irvine, California, Oct. 27-31, 2002. Selected as best paper of the Flight Critical Systems track.