Digital Flight Control Systems

Autopilots are very useful. Given modern technology they get better but complexity leads to problems which can be subtle and fatal. The first micro to control an aircraft flew in the Grumman F-14 Tomcat. It is written up in the First Microprocessor, The General Dynamics F-16 Fighting Falcon has triple micros to give greater reliability. The chance of two random hardware failures at the same time is much smaller than that of one. That is the pay off. The disadvantage is that the three devices are checking each other so software has to deal with what John Rushby referred to as Byzantine complexity that is to say unforeseen causes of disagreement which lead to healthy hardware being rejected. If one fails the other two can carry on. If a micro gives misleading information to the others problems arise. Earlier systems had fall back controllers which took over when things went wrong.

One answer is to keep things as simple as possible. The right answer may be Machiavellian cunning although Doctor Rushby advocates the use of formal logic in Formal Verification of Algorithms for Critical Systems. It not necessarily easy but it should give answers which are provably correct.

First Microprocessor
QUOTE
The F-14A “Tom Cat” Microprocessor
The first microprocessor was designed and developed from 1968-1970.  This site describes the design work for a MOS-LSI, highly integrated, microprocessor chip set designed starting June 1968 and completed by June 1970. This highly integrated computer chip set was designed for the US Navy F14A “TomCat” fighter jet by Mr. Steve Geller and Mr. Ray Holt while working for Garrett AiResearch Corp under contract from Grumman Aircraft, the prime contractor for the US Navy. The MOS-LSI chips were manufactured by American Microsystems, Inc of Santa Clara, California.

The MOS-LSI chip set was part of the Central Air Data Computer (CADC) which had the function of controlling the moving surfaces of the aircraft and the displaying of pilot information. The CADC received input from five sources, 1) static pressure sensor, dynamic pressure sensor, analog pilot information, temperature probe, and digital switch pilot input. The output of the CADC controlled the moving surfaces of the aircraft. These were the wings, maneuver flaps, and the glove vane controls. The CADC also controlled four cockpit displays for Mach Speed, Altitude, Air Speed, and Vertical Speed. The CADC was a redundant system with real-time self-testing built-in. Any single failure from one system would switch over to the other.

Two state-of-the-art quartz sensors, a 20-bit high precision analog-to-digital converter, a 20-bit high precision digital-to-analog converter, the MOS-LSI chip set, and a very efficient power unit made up the complete CADC. A team of over 25 managers, engineers, programmers, and technicians from AiResearch and American Microsystems labored for three years to accomplish a design feat never before attempted, a complete state-of-the-art, highly integrated, digital air data computer. Previous designs were based around mechanical technology, consisting of precision gears and cams.

In 1971, Mr. Ray Holt wrote a design paper on the MOS-LSI chip set design which was approved for publication by Computer Design magazine. However, because of national security reasons the U.S. Navy would not approve this paper for publication. Mr. Holt attempted again in 1985 to have the paper cleared and the answer again was no. Finally, in April 1997, he started the process again and this time was able to receive clearance for publication as of April 21, 1998.

The entire contents of this original 1971 paper, “Architecture Of A Microprocessor“, is made available here. The first public announcement of the F14A MOS-LSI microprocessor chip set was a published article by the Wall Street Journal on September 22, 1998. This paper and the details of the design were first presented publicly by Mr. Ray Holt at the Vintage Computer Festival held at the Santa Clara Convention Center on September 26-27, 1998.

Many thanks to Mr. Sam Ismail of the Vintage Computer Festival for, not only his believability of this design, but for his hard work in making it a significant announcement in the microprocessor world.
UNQUOTE
Military development is a big driver in the research field.

 

http://www.firstmicroprocessor.com/documents/lsistate-97.pdf
Is worth a look.

 

Formal Verification of Algorithms for Critical Systems
QUOTE
We describe our experience with formal, machine-checked verification of algorithms for critical applications, concentrating on a Byzantine fault-tolerant algorithm for synchronizing the clocks in the replicated computers of a digital flight control system. First, we explain the problems encountered in unsynchronized systems and the necessity, and criticality, of fault-tolerant synchronization. We give an overview of one such algorithm, and of the arguments for its correctness. Next, we describe a verification of the algorithm that we performed using our EHDM system for formal specification and verification. We indicate the errors we found in the published analysis of the algorithm, and other benefits that we derived from the verification. Based on our experience, we derive some key requirements for a formal specification and verification system adequate to the task of verifying algorithms of the type considered. Finally, we summarize our conclusions regarding the benefits of formal verification in this domain, and the capabilities required of verification systems in order to realize those benefits.
UNQUOTE
Unfortunately the rest is inaccessible without paying an exorbitant fee.

 

http://www.csl.sri.com/users/rushby/anomalies.html  http://www.nationalmuseum.af.mil/factsheets/factsheet.asp?id=612     

3. AFTI/F-16 Flight Test Results and Lessons

4. Design Implications from AFTI/F-16 Flight Test

5. F-16 Versions - F-16 AFTI :: F-16.net

6. AFTI/F-16 History :: F-16.net

Formal verification of algorithms for critical systems by John M Rushby IEEE transactions on software engineering vol 19 no 1 January 1993 page 16 - 1st 2 mistakes non-faulty typo maths too

reaching agreements in the presence of faults http://www.mendeley.com/research/formal-verification-algorithms-critical-systems-1/ terry jones