Publisher's Synopsis
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. Rushby, John Unspecified Center AIRBORNE/SPACEBORNE COMPUTERS; AIRCRAFT EQUIPMENT; DIGITAL SYSTEMS; FAULT TOLERANCE; FLIGHT CONTROL; MATHEMATICAL MODELS; ACTUATORS; AIRCRAFT SPECIFICATIONS; EQUIPMENT SPECIFICATIONS; FAULT TREES; PROVING; THEOREM PROVING...
