Aspects of a draft version of the Aeronautical Telecommunications Network (ATN) Standards and Recommended Practices (SARPs) under development by ISO-compliant committees of the International Civil Aviation Organization (ICAO) have been mathematically modelled using a formal description technique. The ATN SARPs are a specification for a global telecommunications network for air traffic control systems. A version of Harel’s statecharts formalism embedded within a machine readable typed predicate logic has been used as a formal description technique to construct this mathematical model. Our model has been `typechecked’ to partially validate the internal consistency of the specification. The work described in this paper has already uncovered some problems in the draft SARPs, and will provide a basis for follow-on efforts to apply formal analysis methods such as model-checking and symbolic execution to aspects of the ATN SARPs. The success of this approach suggests that typed predicate logic is useful as a syntactic and semantic foundation for specialized Formal Description Techniques (FDTs).

Original document

The different versions of the original document can be found in:

Back to Top

Document information

Published on 01/01/2013

Volume 2013, 2013
DOI: 10.1007/978-0-387-35271-8_26
Licence: CC BY-NC-SA license

Document Score


Views 1
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?