The Boeing Company was sponsored by NASA Langley to develop advanced validation and verification techniques for fly-by-wire systems. As part of the project, Boeing explored the use of formal methods. The goal of this work was two-fold:
The first phase of this project focused on the formal verification of ``real'' hardware devices using the HOL hardware verification methodology. With the assistance of a subcontract with U. C. Davis, Boeing partially verified a set of hardware devices, including a microprocessor, a floating-point coprocessor similar to the Intel 8087 but smaller, a direct memory access (DMA) controller similar to the Intel 8237A but smaller, and a set of memory-management units. U. C. Davis also developed the generic-interpreter theory to aid in the formal specification and verification of hardware devices, and a horizontal-integration theory for composing verified devices into a system.
After demonstrating the feasibility of verifying standard hardware devices, Boeing applied the methodology to a set of proprietary hardware devices being developed at Boeing for use in a number of aeronautics and space applications. NASA sponsored a Boeing engineer to work with the Processor Interface Unit (PIU) design team to formally specify and verify the device.
Boeing and U.C. Davis also performed an assessment of the the U.K. Royal Signals and Radar Establishment's (RSRE) VIPER chip VIPER. This was part of a now-completed 3 year Memorandum of Understanding (MOU) with RSRE. CLI and Langley researchers also performed assessments of the VIPER project.
Application of formal methods to the suite of Intel-like devices and the PIU demonstrated that formal methods can be practically applied to the digital hardware devices being developed by Boeing today and provided insight on how to make the process more cost effective.