Formal Methods in the Aerospace Industry: Follow the Money

Abstract

Modern aircraft contain millions of lines of complex software, much of it performing functions that are critical to safe flight. This software must be verified to function correctly with the highest levels of assurance, and aircraft manufacturers must demonstrate evidence of correctness through a rigorous certification process. Furthermore, the size and complexity of the on-board software are rising exponentially. Current test-based verification methods are becoming more expensive and account for a large fraction of the software development cost. New approaches to verification are needed to cope effectively with the software being developed for next-generation aircraft.

Formal analysis methods such as model checking permit software design models to be evaluated much more completely than is possible through simulation or test. This permits design defects to be identified and eliminated early in the development process, when they have much lower impact on cost and schedule. Advances in model checking technology, the adoption of model-based software development processes, and new certification guidance are enabling formal methods to be used by the aerospace industry for verification of software.

This talk provides an overview of our work applying formal methods, such as model checking, to the development of software for commercial and military aircraft [1]. Formal methods being used to provide increased assurance of correctness, reduce development cost, and satisfy certification objectives. A number of applications of formal methods at Rockwell Collins will be presented to illustrate these benefits and how they relate to the aerospace industry.

The traditional justification for the use of formal methods has been to provide increased assurance of correctness, especially for systems or components that implement safety-critical functions. Model checking excels in this area, providing comprehensive exploration of system behavior and exposure of design errors.

However, the strongest motivation for adoption of model checking in the industry seems much more likely to be cost reduction [2]. The ability to detect and eliminate defects early in the development process has a clear impact on downstream costs. Errors are much easier and cheaper to correct in the requirements and design phases than during subsequent implementation and integration phases.

An additional benefit which may become increasingly important is the ability to satisfy certification objectives through the use of formal methods, including model checking. New certification guidance supporting the use of formal methods has been included in the recently published DO-178C [3], the industry standard governing software aspects of aircraft certification. This will also impact the economic motivations surrounding the use of formal methods.