Refinement for Fault-Tolerance: An Aircraft Hand-Off Protocol
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 1994
- Accession Number
- ADA278004
Entities
People
- Fred B. Schneider
- Jon Dehn
- Keith Marzullo
Organizations
- Cornell University