FCS 5000 Mode Logic Analysis

Formal Verification of Flight Critical Software (Powerpoint Presentation)

The FCS 5000 is a family of Flight Control Systems (FCS) being developed by Rockwell Collins Inc. for use in business and regional jet aircraft. The mode logic of the Flight Guidance System (FGS) is an important component of the FCS 5000 architecture that determines which lateral and vertical flight modes are to be armed and active at any time. The mode logic of the FGS is particularly difficult to design and verify. To address this, the FCS 5000 team has made use of the advanced verification technologies developed under the MT-FCS project.

The FCS 5000 mode logic analyzed consists of five mode transitions diagrams, each considerably larger than the example shown above. There are 36 modes, 172 events, and 488 transitions distributed roughly equally among the five diagrams. The events are typically guarded by Boolean expressions, and the guards of different events often share the same input values. Changes in the state of a mode diagram usually affect at least one, and often more, of the other mode diagrams. While each individual diagram is quite clear and straightforward to understand, grasping all the possible interactions is very difficult to do manually.

Formal verification of the mode logic found 26 errors. Of these, 17 were found through model checking, six were found by creating the model, and three were found by inspection prior to creating the model. Of the 26 errors, 18 would have been unlikely to have been found by traditional verification methods.

However, one of the greatest benefits of this approach is that the errors were discovered early in life-cycle during requirements analysis.

Publications Related to the Analysis of Mode Logic

• 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.
• 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.