Abstract
Departure routine is essential part in the air traffic control and must be formally designed to avoid potential hazards and to verify proper functioning of the underlying processes. This paper addresses the Petri net approach to formally model the departure routine of the aircraft which ensures the organized flow of air traffic during departure. First, the high-level design of the system is presented by identifying key objects involved in departure routine, and then, its detailed model is presented. Moreover, the verification of the underlying methodology has been made using coverability tree. The proposed model is verified to be safe (bounded), potentially reversible and deadlock free which ensures reliability of the system and guarantees the efficient and controlled communication between the aircraft and local and ground controllers.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Issues in Air Traffic Control. http://www.academon.com/term-paper/issues-in-airtraffic-control-149962/. January 2012; Retrieved Sept 2012
U.S. Department of Transportation. Federal Aviation Administration. Order JO 7110.65u. http://www.faa.gov/documentLibrary/media/Order/7110.65UBasic.pdf. Retrieved Feb 2013
U.S. Department of Transportation. Federal Aviation Administration. Order JO 7110.65u, air traffic control chapter 2, section 1: general control. http://www.faa.gov/air_traffic/publications/atpubs/ATC/atc0201.html. Retrieved Feb 2013
Oberheid H, Söffker D (2008) Cooperative arrival management in air traffic control—a coloured Petri net model of sequence planning. In: Proceedings of the 29th international conference on applications and theory of Petri nets. Petri nets 2008, pp 348–367
Hanh TTB, Hung DV (2007) Verification of an air traffic control system with probabilistic real time model-checking. UNU-IIST report
U. S. Department of Transportation. Federal Aviation Administration. Aeronautical Information Manual. Air traffic procedures chapter 5, section 2: departure procedures. http://www.faa.gov/air_traffic/publications/atpubs/aim/aim0502.html#aim0502.html.1. Retrieved Feb 2013
Hollnagel E (2009) The ETTO principle: efficiency-thoroughness trade-off—why things that go right sometimes go wrong. Ashgate, Farnham
Stroeve SH, Everdij MHC, Blom HAP (2011) Studying hazards for resilience modeling in ATM. Mathematical Approach towards Resilience Engineering in ATM (MAREA) 2011; First SESAR Innovation Days: Ecole Nationale de l’Aviation Civile (ENAC). Toulouse, France
Smieszek H (2012) Modeling behavior and performance of air traffic controllers using coloured petri nets. Technische Universität Berlin, Centre of Human-Machine Systems, Berlin
Benediktsson O, Hunter RB, McGettrick AD (2001) Processes for software in safety critical systems. Software IEEE 6(1):47–62
Communication and Air Traffic Communication and Air Traffic Safety. http://www.academon.com/analytical-essay/communication-and-air-traffic-safety-146602/. January 2011; Retrieved Jan 2013
Hossein N (2008) Modeling activities diagram to colored Petri net for validation and verification based on non functional parameters. Master thesis, Faculty of Computer Science and Information Systems, University Technology Malaysia
Luciano Baresi B, Mauro P (2001) Improving UML with Petri nets. Electron Notes Theor Comput Sci 44(4):107–119
Ahmad F, Huang HJ, Wang XL (2011) Analysis of the Petri net model of parallel manufacturing processes with shared resources. Inf Sci 181:5249–5266
Ahmad F, Khan SA (2012) Module-based architecture for periodic job-shop scheduling problem. Comput Math Appl 64(1):1–10
Khan SA, Zafar NA, Ahmad F (2011) Petri net modeling of railway crossing system using fuzzy brakes. Int J Phys Sci 6(14):3389–3397
Jing M, Lu W (2002) Extension of UML and its conversion to Petri nets for semiconductor manufacturing modeling. IEEE 3:3175–3180
Lopez-Grao JP, Jose M, Javier C From UML activity diagrams to stochastic Petri nets: application to software performance engineering. In: Proceedings of the seventeenth international symposium on computer and information sciences. CRC Press, pp 25–36
Ahmad F, Khan SA (2013) Specification and verification of safety properties along a crossing region in a railway network control. Appl Math Model 37(7):5162–5170
Ali G, Khan SA, Ahmad F, Zafar NA (2012) Visualized and abstract formal modeling towards the multi-agent systems. Int J Basic Appl Sci 2(8):8272–8284
Ali G, Khan SA, Ahmad F, Zafar NA (2012) Formal modeling towards a dynamic organization of multi-agent systems using communicating X-machine and Z-notation. Indian J Sci Technol 5(7):2972–2977
Khan SA, Zafar NA (2011) Extending promotion for the management of moving block interlocking components. Int J Phys Sci 6(31):7262–7270
Khan SA, Zafar NA (2007) Promotion of local to global operation in train control system. J Digit Inf Manag 5(4):228–233
Herencia-Zapana H, Hagen G, Neogi N (2012) A framework for probabilistic evaluation of interval management tolerence in the terminal radar control area. In: IEEE 2012 digital avionics systems conference (DASC), Oct 2012, pp 9E1-1–9E1-8
Yousaf S, Zafar NA, Khan SA (2010) Formal analysis of departure procedure of air traffic control system. In: IEEE 2010 on software technology and engineering (ICSTE), Oct 2010, vol 2, pp 301–305
Horl J, Aichernig BK (2008) Requirements validation of a voice communication system used in air traffic control. An industrial application of light weight formal methods. In. IEEE 208 symposium on reliable distributed systems, Oct 2008, pp 95–104
Jamal M, Zafar NA (2007) Requirements analysis of air traffic control system using formal methods. J Indep Stud Res 5(2):1–7
Butler RW, Maddalon J, Geser A, Muñoz CA (2003) Simulation and verification: formal analysis of air traffic management systems: the case of conflict resolution and recovery. In: Winter simulation conference, Dec 2003, pp 906–914
Leadbeter D, Lindsay P, Hussey A, Neal A, Humphreys M (2000) Integrating the operator into formal models in the air traffic control domain. Technical report
Horl J, Aichernig BK (1999) Formal specification of voice communication system used in air traffic control system. World congress on formal methods in the development of computing systems. Springer, 2
Fung F, Damir J (1998) Formal specification of a flight guidance system. Technical report. NASA
Smieszek H (2012) Modeling behavior and performance of air traffic controllers using coloured petri nets. Technische Universitäte Berlin, Centre of Human-Machine Systems, Berlin
Smieszek H, Karl C (2013) An approach to cognitive simulation of air traffic controllers based on coloured petri nets. Research Report: Technical University of Berlin, Germany
Davidrajuh R, Lin B (2011) Exploring airport traffic capability using Petri net based model. Expert Syst Appl 38(9):10923–10931
Liu C, Zhang L (2010) Modeling and simulating on flight push-out conflicts based on colored Petri net. In: Control conference (CCC) 2010, July 2010, pp 5447–5452
Sun S, Hua K (2009) An aircraft sequencing approach based on fuzzy Petri-net. In: International joint conference 2009 computational sciences and optimization, pp 1008–1011
Oberheid H, Söffker D (2008) Cooperative arrival management in air traffic control—a coloured Petri net model of sequence planning. In: 29th IEEE 2008 applications and theory of Petri nets, Springer, pp 348–367
Kovács Á, Németh E, Hangos KM (2005) Modeling and optimization of runway traffic flow using coloured Petri nets. In: IEEE 2005 control and automation, 2005, vol 2, pp 881–886
Vismari LF, Camargo JB (2008) An absolute—relative risk assessment methodology approach to current safety critical systems and its application to the ADS-B based air traffic control system. In: ICRE 2008, Oct 2008, pp 95–104
Everdij MHC, Blom HAP, Klompstra MB (1997) Dynamically coloured Petri nets for air traffic management safety purposes. In: 8th IFAC symposium on transportation systems 1997, New York
Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4):541–580
Reisig W (1985) Petri nets: an introduction. Springer, Heidelberg
Pntoolbox: “Petri net toolbox for MATLAB” v2.3.1, http://www.ac.tuiasi.ro/pntool/. Retrieved Feb 2013
Pelayo FL, Valverde JC (2012) Notes on modeling dynamics of concurrent computing systems. Comput Math Appl 64:61–63
Guirao JLG, Pelayo FL, Valverde JC (2011) Modeling dynamics of concurrent computing systems. Comput Math Appl 61:1402–1406
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Sadiq, A., Ahmad, F., Khan, S.A. et al. Modeling and analysis of departure routine in air traffic control based on Petri nets. Neural Comput & Applic 25, 1099–1109 (2014). https://doi.org/10.1007/s00521-014-1590-4
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00521-014-1590-4