Abstract

We propose a general formal modeling and verification of the air traffic control system (ATC). This study is based on the International Civil Aviation Organization (ICAO), Federal Aviation Administration (FAA), and National Aeronautics and Space Administration (NASA) standards and recommendations. It provides a sophisticated assistance system that helps in visualizing aircrafts and presents automatic bugs detection. In such a critical safety system, the use of robust formal methods that assure bugs absence is highly required. Therefore, this work suggests a formalism of discrete transition systems based on abstraction and refinement along proofs. These ensure the consistency of the system by means of invariants preservation and deadlock freedom. Hence, all invariants hold permanently providing a handy solution for bugs absence verification. It follows that the said deadlock freedom ensures a continuous running of a given system. This specification and modeling technique enable the system to be corrected by construction.

Document type: Article

Full document

The PDF file did not load properly or your web browser does not support viewing PDF files. Download directly to your device: Download PDF document

Original document

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

http://downloads.hindawi.com/journals/mse/2018/1692432.xml,
http://dx.doi.org/10.1155/2018/1692432 under the license cc-by
https://doaj.org/toc/1687-5591,
https://doaj.org/toc/1687-5605 under the license http://creativecommons.org/licenses/by/4.0/
http://downloads.hindawi.com/journals/mse/2018/1692432.pdf,
https://academic.microsoft.com/#/detail/2892342489
Back to Top

Document information

Published on 01/01/2018

Volume 2018, 2018
DOI: 10.1155/2018/1692432
Licence: Other

Document Score

0

Views 7
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?