m (Scipediacontent moved page Draft Content 901448322 to Andrews et al 2013a) |
|||
Line 2: | Line 2: | ||
== Abstract == | == Abstract == | ||
− | 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 | + | 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). |
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
Line 15: | Line 10: | ||
* [https://link.springer.com/content/pdf/10.1007%2F978-0-387-35271-8_26.pdf https://link.springer.com/content/pdf/10.1007%2F978-0-387-35271-8_26.pdf] | * [https://link.springer.com/content/pdf/10.1007%2F978-0-387-35271-8_26.pdf https://link.springer.com/content/pdf/10.1007%2F978-0-387-35271-8_26.pdf] | ||
+ | |||
+ | * [http://link.springer.com/content/pdf/10.1007/978-0-387-35271-8_26 http://link.springer.com/content/pdf/10.1007/978-0-387-35271-8_26], | ||
+ | : [http://dx.doi.org/10.1007/978-0-387-35271-8_26 http://dx.doi.org/10.1007/978-0-387-35271-8_26] | ||
+ | |||
+ | * [https://link.springer.com/chapter/10.1007/978-0-387-35271-8_26 https://link.springer.com/chapter/10.1007/978-0-387-35271-8_26], | ||
+ | : [http://core.ac.uk/display/23703805 http://core.ac.uk/display/23703805], | ||
+ | : [https://www.scipedia.com/public/Andrews_et_al_2013a https://www.scipedia.com/public/Andrews_et_al_2013a], | ||
+ | : [https://dblp.uni-trier.de/db/conf/forte/forte1997.html#AndrewsDJ97 https://dblp.uni-trier.de/db/conf/forte/forte1997.html#AndrewsDJ97], | ||
+ | : [https://rd.springer.com/chapter/10.1007/978-0-387-35271-8_26 https://rd.springer.com/chapter/10.1007/978-0-387-35271-8_26], | ||
+ | : [https://academic.microsoft.com/#/detail/1511289226 https://academic.microsoft.com/#/detail/1511289226] |
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).
The different versions of the original document can be found in:
Published on 01/01/2013
Volume 2013, 2013
DOI: 10.1007/978-0-387-35271-8_26
Licence: CC BY-NC-SA license
Are you one of the authors of this document?