Verifying the Safety of a Flight-Critical System
This work addresses safety verification for flight-critical systems, which is crucial for aviation safety, but it is incremental as it applies existing verification methods to a new, complex dataset.
The researchers tackled the challenge of verifying the safety of a flight-critical aircraft control system by applying formal verification technologies, resulting in a successful demonstration on a realistic system that took several person-months to complete.
This paper describes our work on demonstrating verification technologies on a flight-critical system of realistic functionality, size, and complexity. Our work targeted a commercial aircraft control system named Transport Class Model (TCM), and involved several stages: formalizing and disambiguating requirements in collaboration with do- main experts; processing models for their use by formal verification tools; applying compositional techniques at the architectural and component level to scale verification. Performed in the context of a major NASA milestone, this study of formal verification in practice is one of the most challenging that our group has performed, and it took several person months to complete it. This paper describes the methodology that we followed and the lessons that we learned.