Refinement for Fault-Tolerance: An Aircraft Hand-off Protocol

  • Keith Marzullo
  • Fred B. Schneider
  • Jon Dehn
Part of the The Springer International Series in Engineering and Computer Science book series (SECS, volume 284)


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.


Regular Expression Finite State Machine Assignment Statement Proof Outline Interprocess Communication 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    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
  2. [2]
    C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10):576–580 (October 1969).MATHCrossRefGoogle Scholar
  3. [3]
    Richard D. Schlichting and Fred B. Schneider. Fail-Stop Processors: An Approach to Designing Fault-Tolerant Computing Systems. ACM Transactions on Computer Systems 3(1):222–238 (August 1983).CrossRefGoogle Scholar
  4. [4]
    Fred B. Schneider. On Concurrent Programming. To appear.Google Scholar

Copyright information

© Kluwer Academic Publishers 1994

Authors and Affiliations

  • Keith Marzullo
    • 1
  • Fred B. Schneider
    • 2
  • Jon Dehn
    • 3
  1. 1.Department of Computer ScienceUniversity of California San DiegoLa Jolla
  2. 2.Department of Computer ScienceCornell UniversityIthaca
  3. 3.Loral Federal SystemsRockville

Personalised recommendations