Z Specification of Gate and Apron Control Management at Airport
Modelling of an air traffic control (ATC) system is an open issue and has become a challenging problem due to its complexity and increase of traffic at airports and in airspace. Consequently, automated ATC systems are suggested to improve efficiency ensuring the safety standards. It is reported that...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2014-01-01
|
| Series: | Abstract and Applied Analysis |
| Online Access: | http://dx.doi.org/10.1155/2014/530619 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832565569911521280 |
|---|---|
| author | Nazir Ahmad Zafar Fahad Alhumaidan Sher Afzal Khan |
| author_facet | Nazir Ahmad Zafar Fahad Alhumaidan Sher Afzal Khan |
| author_sort | Nazir Ahmad Zafar |
| collection | DOAJ |
| description | Modelling of an air traffic control (ATC) system is an open issue and has become a challenging problem due to its complexity and increase of traffic at airports and in airspace. Consequently, automated ATC systems are suggested to improve efficiency ensuring the safety standards. It is reported that the number of collisions that occurred at airports surface is three times larger than in airspace. Further, it is observed that gates and aprons congestions cause significant delays at airports; hence, effective monitoring and guidance mechanisms are required to control ground air traffic. In this paper, formal procedure of managing air traffic from gate to enter in the active area of airport for taxiing is provided using Z notation. An integration of gate and apron controllers is described to manipulate the information for correct decision making and flow management. Graph theory is used for representation of airport topology and appropriate routs. In static part of the model, safety properties are described in terms of invariants over the critical data types. In dynamic model, the state space is updated by defining pre- and postconditions ensuring the safety. Formal specification is analysed using Z/Eves tool. |
| format | Article |
| id | doaj-art-300ad1be0c9748bcad8897a0d0a2cf94 |
| institution | Kabale University |
| issn | 1085-3375 1687-0409 |
| language | English |
| publishDate | 2014-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Abstract and Applied Analysis |
| spelling | doaj-art-300ad1be0c9748bcad8897a0d0a2cf942025-02-03T01:07:14ZengWileyAbstract and Applied Analysis1085-33751687-04092014-01-01201410.1155/2014/530619530619Z Specification of Gate and Apron Control Management at AirportNazir Ahmad Zafar0Fahad Alhumaidan1Sher Afzal Khan2College of Computer Sciences and IT, King Faisal University, Alahsa 31982, Saudi ArabiaCollege of Computer Sciences and IT, King Faisal University, Alahsa 31982, Saudi ArabiaDepartment of Computer Sciences, Abdul Wali Khan University, Mardan 23200, PakistanModelling of an air traffic control (ATC) system is an open issue and has become a challenging problem due to its complexity and increase of traffic at airports and in airspace. Consequently, automated ATC systems are suggested to improve efficiency ensuring the safety standards. It is reported that the number of collisions that occurred at airports surface is three times larger than in airspace. Further, it is observed that gates and aprons congestions cause significant delays at airports; hence, effective monitoring and guidance mechanisms are required to control ground air traffic. In this paper, formal procedure of managing air traffic from gate to enter in the active area of airport for taxiing is provided using Z notation. An integration of gate and apron controllers is described to manipulate the information for correct decision making and flow management. Graph theory is used for representation of airport topology and appropriate routs. In static part of the model, safety properties are described in terms of invariants over the critical data types. In dynamic model, the state space is updated by defining pre- and postconditions ensuring the safety. Formal specification is analysed using Z/Eves tool.http://dx.doi.org/10.1155/2014/530619 |
| spellingShingle | Nazir Ahmad Zafar Fahad Alhumaidan Sher Afzal Khan Z Specification of Gate and Apron Control Management at Airport Abstract and Applied Analysis |
| title | Z Specification of Gate and Apron Control Management at Airport |
| title_full | Z Specification of Gate and Apron Control Management at Airport |
| title_fullStr | Z Specification of Gate and Apron Control Management at Airport |
| title_full_unstemmed | Z Specification of Gate and Apron Control Management at Airport |
| title_short | Z Specification of Gate and Apron Control Management at Airport |
| title_sort | z specification of gate and apron control management at airport |
| url | http://dx.doi.org/10.1155/2014/530619 |
| work_keys_str_mv | AT nazirahmadzafar zspecificationofgateandaproncontrolmanagementatairport AT fahadalhumaidan zspecificationofgateandaproncontrolmanagementatairport AT sherafzalkhan zspecificationofgateandaproncontrolmanagementatairport |