SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems
 by John Rushby.

From Technical Report CSL-91-3.
June, 1991.

Abstract:

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.
BibTEX entry:

@techreport{csl-91-3,
    AUTHOR = {John Rushby},
    TITLE = {Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems},
    YEAR = {1991},
    MONTH = {jun},
    URL = {http://www.csl.sri.com/papers/csl-91-3/},
    BOOKTITLE = {Technical Report {CSL-91-3}}
}

Download:


csl-91-3.ps.gz

Compressed PostScript

csl-91-3.dvi.gz

Compressed DVI


 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy