Abstract

traffic management system is a complex adaptive and safety critical system which requires considerable attention for its modelling and verification. Currently Air traffic control (ATC) systems are heavily dependent upon human intervention at airport causing accidents and delays because of failure of communication. The purpose of this study is to develop, plan, manage and verify aircrafts movement procedures at the airport surface that prevent delays and collisions. The airport surface is decomposed into blocks and represented by the graph relation. The state space of the system is described by identifying all the possible components of the system. The ground and local controls monitor queues of the aircrafts moving from taxiway to take-off. It is insured that once an aircraft is inserted into a queue, it is eventually removed from it after the next queue has become available. The take-off procedure is provided using graph theory and Vienna Development Method Specification Language (VDM-SL) and analyzed using VDM-SL toolbox. Formal specification of graph-based model, taxiways, aircrafts, runways and controllers is provided in static part of the model. The state space analysis describing take-off algorithms is provided by defining optimal paths and possible operations in dynamic model expediting the departure procedure. The model is developed by a series of refinements following the stepwise development approach. The delays at airport surface require effective safety and guidance protocols to control air traffic at the airport. In static model, the safety criteria are described in terms of invariants over the data types carrying critical information. The safety is insured by defining pre/post conditions in description of operations for changing state space of the system. Although the proposed study is focussed more on the safety component, however, the efficiency is not ignored.

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://link.springer.com/article/10.1186/s40294-016-0014-y/fulltext.html,
http://link.springer.com/content/pdf/10.1186/s40294-016-0014-y,
http://dx.doi.org/10.1186/s40294-016-0014-y under the license cc-by
https://link.springer.com/article/10.1186/s40294-016-0014-y,
https://casmodeling.springeropen.com/articles/10.1186/s40294-016-0014-y,
https://casmodeling.springeropen.com/track/pdf/10.1186/s40294-016-0014-y,
https://core.ac.uk/display/81287731,
https://dblp.uni-trier.de/db/journals/casm/casm4.html#Zafar16,
https://paperity.org/p/75301877/formal-specification-and-analysis-of-take-off-procedure-using-vdm-sl,
https://academic.microsoft.com/#/detail/2280223496 under the license http://creativecommons.org/licenses/by/4.0
Back to Top

Document information

Published on 01/01/2016

Volume 2016, 2016
DOI: 10.1186/s40294-016-0014-y
Licence: Other

Document Score

0

Views 1
Recommendations 0

Share this document

Keywords

claim authorship

Are you one of the authors of this document?