Aircraft Certification Contributions

Certification of new aircraft with digital fly-by-wire flight control systems, especially for civilian airline service, requires software designs that pro­vide highly reliable, predictable, and repeatable performance. For this reason, NASA experts concluded that a comprehensive understanding of all possible software system behaviors is essential, especially in the case of highly complex systems. This knowledge base must be formally docu­mented and accurately communicated for both design and system certifi­cation purposes. This was highlighted in a 1993 research paper sponsored by NASA and the Federal Aviation Administration (FAA) that noted:

This formal documentation process would prove to be a tre­mendously difficult and challenging task. It was only feasible if the underlying software was rationally designed using prin­ciples of abstraction, layering, information-hiding, and any other technique that can advance the intellectual manage­ability of the task. This calls strongly for an architecture that promotes separation of concerns (whose lack seems to be the main weakness of asynchronous designs), and for a method of description that exposes the rationale for design decisions and that allows, in principle, the behavior of the system to be calculated (i. e., predicted or, in the limit, proved) . . . formal methods can make their strongest contribution to quality assur­ance for ultra-dependable systems: they address (as nothing else does) [NASA engineer Dale] Mackall’s plea for ‘a method to make system designs more understandable, more visible.'[1205]

Formal software development methodologies for critical aeronautical and space systems developments have been implemented within NASA and are contained in certification guidebooks and other documents for use by those involved in mission critical computer and software systems.[1206] Designed to help transition Formal Methods from experimental use into
practical application for critical software requirements and systems design within NASA, they discuss technical issues involved in applying Formal Methods techniques to aerospace and avionics software systems. Dryden’s flight-test experience and the observations obtained from flight­testing of such systems were exceptionally well-documented and would prove to be highly relevant to NASA, the FAA, and military service pro­grams oriented to developing Formal Methods and structured approaches in the design, development, verification, validation, testing, and certifica­tion of aircraft with advanced digital flight control systems.[1207] The NASA DFBW F-8 and AFTI/F-16 experiences (among many others) were also used as background by Government and industry experts tasked with preparing the FAA Digital Systems Validation Handbook. Today, the FAA uses Formal Methods in the specification and verification of software and hardware requirements, designs, and implementations; in the identification of the benefits, weaknesses, and difficulties in applying these Formal Methods to digital systems used in critical applications; and in support of aircraft software systems certification.