Towards Sophisticated Air Traffic Control System Using Formal Methods
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. I...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2018-01-01
|
| Series: | Modelling and Simulation in Engineering |
| Online Access: | http://dx.doi.org/10.1155/2018/1692432 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832567168147914752 |
|---|---|
| author | Abdessamad Jarrar Youssef Balouki |
| author_facet | Abdessamad Jarrar Youssef Balouki |
| author_sort | Abdessamad Jarrar |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-489a02bd031d4c2984f98ae32231a81b |
| institution | Kabale University |
| issn | 1687-5591 1687-5605 |
| language | English |
| publishDate | 2018-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Modelling and Simulation in Engineering |
| spelling | doaj-art-489a02bd031d4c2984f98ae32231a81b2025-02-03T01:02:09ZengWileyModelling and Simulation in Engineering1687-55911687-56052018-01-01201810.1155/2018/16924321692432Towards Sophisticated Air Traffic Control System Using Formal MethodsAbdessamad Jarrar0Youssef Balouki1Faculty of Sciences and Technologies of Settat, Computing, Imaging and Modeling of Complex Systems Laboratory, Hassan 1st University, Settat, MoroccoFaculty of Sciences and Technologies of Settat, Computing, Imaging and Modeling of Complex Systems Laboratory, Hassan 1st University, Settat, MoroccoWe 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.http://dx.doi.org/10.1155/2018/1692432 |
| spellingShingle | Abdessamad Jarrar Youssef Balouki Towards Sophisticated Air Traffic Control System Using Formal Methods Modelling and Simulation in Engineering |
| title | Towards Sophisticated Air Traffic Control System Using Formal Methods |
| title_full | Towards Sophisticated Air Traffic Control System Using Formal Methods |
| title_fullStr | Towards Sophisticated Air Traffic Control System Using Formal Methods |
| title_full_unstemmed | Towards Sophisticated Air Traffic Control System Using Formal Methods |
| title_short | Towards Sophisticated Air Traffic Control System Using Formal Methods |
| title_sort | towards sophisticated air traffic control system using formal methods |
| url | http://dx.doi.org/10.1155/2018/1692432 |
| work_keys_str_mv | AT abdessamadjarrar towardssophisticatedairtrafficcontrolsystemusingformalmethods AT youssefbalouki towardssophisticatedairtrafficcontrolsystemusingformalmethods |