Refinement for Fault-Tolerance: An Aircraft Hand-Off Protocol
Keith Marzullo, Fred B. Schneider, Jon Dehn · 1994
Part of the Advanced Automation System (AAS) for air-traffic control is a protocol to permit flight hand-off from one air-traffic controller to another.The protocol must be fault-tolerant and, therefore, is subtle-an ideal candidate for the application of formal methods.This paper describes a formal method for deriving fault-tolerant protocols that is based on refinement and proof outlines.The AAS hand-off protocol was actually derived using this method; that derivation is given.