Formal specification and verification of a fault-masking and transient-recovery model for digital flight-control systems

Author:: Rushby, John
Published:: Jul 1, 1991.
Physical Description:: 1 electronic document

Online Version

hdl.handle.net , Connect to this object online.

Availability

Finding items...

Restrictions on Access:

Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access

Summary:

The formal specification and mechanically checked verification for a model of fault-masking and transient-recovery among the replicated computers of digital flight-control systems are presented. The verification establishes, subject to certain carefully stated assumptions, that faults among the component computers are masked so that commands sent to the actuators are the same as those that would be sent by a single computer that suffers no failures.

Other Subject(s):

COMPUTER SYSTEMS

Collection:

NASA Technical Reports Server (NTRS) Collection.

Note:

Document ID: 19910018554.
Accession ID: 91N27868.
NASA-CR-4384.
NAS 1.26:4384.

Terms of Use and Reproduction:

No Copyright.

View MARC record | catkey: 15680048