paper

SIFT: Design and Analysis of a Fault-Tolerant Computer for Aircraft Control

  • Authors:
Read the paper

📜 Abstract

Abstract—SIFT (Software Implemented Fault Tolerance) is an ultrareliable computer for critical aircraft control applications that achieves fault tolerance by the replication of tasks among processing units. The main processing units are off-the-shelf minicomputers, with standard microcomputers serving as the interface to the I/O system. Fault isolation is achieved by using a specially designed redundant bus system to interconnect the processing units. Error detection and analysis and system reconfiguration are performed by software. Iterative tasks are redundantly executed, and the results of each iteration are voted upon before being used. Thus, any single failure in a processing unit or bus can be tolerated with triplication of tasks, and subsequent failures can be tolerated after reconfiguration. Independent execution by separate processors means that the processors need only be loosely synchronized, and a novel fault-tolerant synchronization method is described. The SIFT software is highly structured and is formally specified using the SRI-developed SPECIAL language. The correctness of SIFT is to be proved using a hierarchy of formal models. A Markov model is used both to analyze the reliability of the system and to serve as the formal requirement for the SIFT design. Axioms are given to characterize the high-level behavior of the system, from which a correctness statement has been proved. An engineering test version of SIFT is currently being built.

✨ Summary

  • SIFT established an early integrated architecture for safety-critical distributed computing in which commodity processors were replicated, task outputs were majority-voted, faults were diagnosed in software, and failed components were bypassed through dynamic reconfiguration.
  • The SIFT project directly contributed to the formulation of the Byzantine generals problem and its agreement algorithms, which became foundational results in Byzantine fault-tolerant distributed computing. (microsoft.com)
  • The paper also presented an early formal-verification approach based on state-transition models and refinement mappings: higher-level reliability and allocation models were related to progressively lower-level software and hardware models. This approach influenced later work on rigorous specification and verification of dependable concurrent systems. (microsoft.com)
  • The SIFT system was subsequently implemented and evaluated in NASA avionics research, while the broader architecture is documented by SRI as an early contribution to distributed fault-tolerant computing. (sri.com)