Refinement for Fault-Tolerance: An Aircraft Hand-off Protocol
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.
KeywordsRegular Expression Finite State Machine Assignment Statement Proof Outline Interprocess Communication
Unable to display preview. Download preview PDF.
- F. Cristian, B. Dancey and J. Dehn. Fault-Tolerance in the Advanced Automation System. In Proceedings of 20th International Symposium on Fault-Tolerant Computing, Newcastle Upon Tyne, UK, 26–28 June 1990), pp. 6–17.Google Scholar
- Fred B. Schneider. On Concurrent Programming. To appear.Google Scholar