From Formal Techniques in Real-Time and Fault-Tolerant Systems, Chapter 5.
Edited by J.Vytopil.
Kluwer International Series in Engineering and Computer Science.
1993.

We present a formal model for fault-masking and transient-recovery among the replicated computers of digital flight-control systems. We establish conditions under which majority voting causes the same commands to be sent to the actuators as those that would be sent by a single computer that suffers no failures. The model and its analysis have been subjected to formal specification and mechanically checked verification using the EHDM system.

@article{unspecified,
    AUTHOR = {John Rushby},
    TITLE = {Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems},
    YEAR = {1993},
    URL = {http://www.csl.sri.com/papers/ftrtft92-jmr/},
    BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
    PUBLISHER = {Kluwer International Series in Engineering and Computer Science},
    CHAPTER = {5},
    EDITOR = {J.Vytopil}
}

• ftrtft92-jmr.dvi.gz
• ftrtft92-jmr.ps.gz