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 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).
Chapter PDF
Similar content being viewed by others
Keywords
References
Cleaveland, R., Parrow, J. and Steffen, B. (1989) A Semantics-Based Verification Tool for Finite State Systems, in Proc. 9th IFIP Symposium on Protocol Specification, Testing and Verification, North-Holland.
Day, Nancy (1993) A model checker for statecharts, M.Sc. thesis, Department of Computer Science, University of British Columbia, Technical Report 93–35
Harel, David (1987) Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8, 231–274.
Heimdahl, Mats P.E. and Leveson, Nancy G. (1996) Completeness and consistency in hierarchical state-based requirements. IEEE Transactions on Software Engineering, 22 (6), 363–377.
Heitmeyer, Constance L., Jeffords, Ralph D. and Labaw, Bruce G. (1996) Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology, 5 (3), 231–261.
ISO (International Organization for Standardization) (1994) ACSE Protocol, ITU-T Rec. X.227 - ISO/IEC 8650–1: Edition 2. Available in electronic format via anonymous FTP at URL `ftp://ftp.stel.com/ pub/atnp2/iv/P2’.
Joyce, J., Day, N. and Donat M. (1994) S: A machine readable specification notation based on higher order logic, in 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications, 285–299.
Leveson, Nancy G., Heimdahl, Mats P. E., Hildreth, Holly and Reese, Jon D. (1994) Requirements Specification for Process-Control Systems. IEEE Transactions on Software Engineering 20(9) 684–107.
SARP (1996) Aeronautical Telecommunication Network Panel. Draft. Available via anonymous FTP at URL `ftp://ftp.stel.com/ pub/atnp2’.
Turner, K. J. (ed) (1993) Using Formal Description Techniques: An Introduction to Estelle, LOTOS and SDL. Wiley.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Andrews, J.H., Day, N.A., Joyce, J.J. (1997). Using a Formal Description Technique to Model Aspects of a Global Air Traffic Telecommunications Network. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds) Formal Description Techniques and Protocol Specification, Testing and Verification. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35271-8_26
Download citation
DOI: https://doi.org/10.1007/978-0-387-35271-8_26
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5260-1
Online ISBN: 978-0-387-35271-8
eBook Packages: Springer Book Archive