Formal specification and analysis of take-off procedure using VDM-SL


== 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 ==
<pdf>Media:Draft_Content_445526828-beopen734-1477-document.pdf</pdf>


== Original document ==

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

* [http://dx.doi.org/10.1186/s40294-016-0014-y http://dx.doi.org/10.1186/s40294-016-0014-y] under the license http://creativecommons.org/licenses/by/4.0

* [https://casmodeling.springeropen.com/track/pdf/10.1186/s40294-016-0014-y https://casmodeling.springeropen.com/track/pdf/10.1186/s40294-016-0014-y] under the license http://creativecommons.org/licenses/by/4.0

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