{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T22:39:53Z","timestamp":1776119993080,"version":"3.50.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,9,3]],"date-time":"2018-09-03T00:00:00Z","timestamp":1535932800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2018,9,3]],"date-time":"2018-09-03T00:00:00Z","timestamp":1535932800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Complex Adapt Syst Model"],"published-print":{"date-parts":[[2018,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Air traffic control system in airports is one of the most complex systems in the context of air traffic management due to the huge number of requirements. In order to help engineers to develop such complex system we propose a predefined model that includes the essence of air traffic control and the standard requirements. We develop this model using the Event-B formal method which is based on set theory and allows theorems proving. Event-B is also hinged on refinement which means starting with an abstract model and then enriching it in successive steps. Event-B has been successfully applied in several transportation systems and shows no bugs. This encourages us to use it in this critical system to guarantee a strong assurance of bugs\u2019 absence and to ensure model correctness. Our approach provides a standard model to start with in order to model any airport control system, which allows engineers to focus on more typical requirements that are not developed here.<\/jats:p>","DOI":"10.1186\/s40294-018-0056-4","type":"journal-article","created":{"date-parts":[[2018,9,3]],"date-time":"2018-09-03T14:40:21Z","timestamp":1535985621000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal modeling of a complex adaptive air traffic control system"],"prefix":"10.1186","volume":"6","author":[{"given":"Abdessamad","family":"Jarrar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Youssef","family":"Balouki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,3]]},"reference":[{"key":"56_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: system and software engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, New York"},{"issue":"6","key":"56_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial JR, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transfer 12(6):447\u2013466","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"56_CR3","doi-asserted-by":"crossref","unstructured":"Belhaj H, Balouki Y, Bouhdadi M, El Hajji S (2010) Using Event B to specify QoS in ODP enterprise language. In: Working conference on virtual enterprises. Springer, Berlin, pp 478\u2013485","DOI":"10.1007\/978-3-642-15961-9_57"},{"issue":"1","key":"56_CR4","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1186\/2194-3206-1-15","volume":"1","author":"S Bouarfa","year":"2013","unstructured":"Bouarfa S, Blom HA, Curran R, Everdij MH (2013) Agent-based modeling and simulation of emergent behavior in air transportation. Compl Adapt Syst Model 1(1):15","journal-title":"Compl Adapt Syst Model"},{"key":"56_CR5","doi-asserted-by":"crossref","unstructured":"Cansell D, M\u00e9ry D, Rehm J (2007) Time constraint patterns for Event B development. In: International conference of B users. Springer, Berlin, pp 140\u2013154","DOI":"10.1007\/11955757_13"},{"issue":"4","key":"56_CR6","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke EM, Wing JM (1996) Formal methods: state of the art and future directions. ACM Comput Surv (CSUR) 28(4):626\u2013643","journal-title":"ACM Comput Surv (CSUR)"},{"key":"56_CR7","unstructured":"Department of transportation federal aviation administration, aeronautical information publication, United States of America (2017) 24 edn, amendment 2"},{"key":"56_CR8","unstructured":"Dominique M, Neeraj KS (2011) EB2J: code generation from Event-B to Java, SBMF. IN: Brazilian symposium on formal methods, S\u00e3o Paulo, Brazil"},{"key":"56_CR9","doi-asserted-by":"crossref","unstructured":"Dominique M, Singh NK (2016) Modeling an aircraft landing system in Event-B. In: International conference on abstract state machines, alloy, B, TLA, VDM, and Z, ABZ 2014 ABZ: the landing Gear case study. Springer, Berlin, pp 154\u2013159","DOI":"10.1007\/978-3-319-07512-9_12"},{"key":"56_CR10","unstructured":"Fact Sheet-FAA & NTSB\u2019s \u201cMost Wanted\u201d Recommendations (2010) https:\/\/www.faa.gov\/news\/fact_sheets\/news_story.cfm?newsId=11186.\u00a0Accessed 20 May 2018"},{"issue":"11\u201312","key":"56_CR11","doi-asserted-by":"publisher","first-page":"879","DOI":"10.1016\/j.scico.2009.07.006","volume":"74","author":"TS Hoang","year":"2009","unstructured":"Hoang TS, Kuruma H, Basin D, Abrial JR (2009) Developing topology discovery in Event-B. Sci Comput Program 74(11\u201312):879\u2013899","journal-title":"Sci Comput Program"},{"key":"56_CR12","unstructured":"iFACTS-Air Traffic Management System (2017) https:\/\/www.adacore.com\/customers\/uks-next-generation-atc-system.\u00a0Accessed 13 May 2018"},{"key":"56_CR13","unstructured":"In Focus: ICAO\u2019S Strategic Objectives (2018) https:\/\/www.icao.int\/Pages\/default.aspx.\u00a0Accessed 10 May 2018"},{"key":"56_CR14","doi-asserted-by":"crossref","unstructured":"Jarrar A et al (2017) Modeling aircraft landing scheduling in Event B. In: International conference on information technology and communication systems. Springer, Berlin, pp 127\u2013142","DOI":"10.1007\/978-3-319-64719-7_12"},{"key":"56_CR15","doi-asserted-by":"crossref","unstructured":"Jarrar A, Balouki Y (2018) Formal reasoning for air traffic control system using Event-B method. In: International conference on computational science and its applications. Springer, Cham, pp 241\u2013252","DOI":"10.1007\/978-3-319-95165-2_17"},{"issue":"4","key":"56_CR16","doi-asserted-by":"crossref","first-page":"2045","DOI":"10.11591\/ijece.v7i4.pp2045-2053","volume":"7","author":"A Jarrar","year":"2017","unstructured":"Jarrar A, Balouki Y, Gadi T (2017) Formal specification of QoS negotiation in ODP system. Int J Elec Comput Eng 7(4):2045","journal-title":"Int J Elec Comput Eng"},{"key":"56_CR17","unstructured":"John S, Duncan (2016) Airplane flying handbook. Department of transportation Federal Aviation Administration Flight Standards Service, FAA-H-8083-38"},{"key":"56_CR18","unstructured":"Lecomte T, Servat T, Pouzancre G (2007) Formal methods in safety-critical railway systems. In: 10th Brasilian symposium on formal methods, pp 29\u201331"},{"key":"56_CR19","doi-asserted-by":"crossref","unstructured":"Luo S, Yu G (1998) Airline schedule perturbation problem: landing and takeoff with nonsplitable resource for the ground delay program. In: Operations research in the airline industry. Springer, Boston, pp 404\u2013432.\u200f","DOI":"10.1007\/978-1-4615-5501-8_14"},{"key":"56_CR20","doi-asserted-by":"crossref","unstructured":"Lygeros J, Lynch N (1997) On the formal verification of the TCAS conflict resolution algorithms. In: Proceedings of the 36th IEEE conference on decision and control. pp 1829\u20131834","DOI":"10.1109\/CDC.1997.657846"},{"key":"56_CR21","doi-asserted-by":"crossref","unstructured":"Narkawicz A, Munoz C (2015) A formally verified conflict detection algorithm for polynomial trajectories. In: AIAA Infotech@ Aerospace. p 0795","DOI":"10.2514\/6.2015-0795"},{"key":"56_CR22","unstructured":"NASA Air Traffic Management Demonstration Goes Live in Charlotte (2017) https:\/\/www.nasa.gov\/aero\/nasa-air-traffic-management-demo-goes-live.\u00a0Accessed 20 May 2018"},{"issue":"2","key":"56_CR23","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1016\/j.ejor.2004.09.040","volume":"171","author":"H Pinol","year":"2006","unstructured":"Pinol H, Beasley JE (2006) Scatter search and bionomic algorithms for the aircraft landing problem. Eur J Oper Res 171(2):439\u2013462","journal-title":"Eur J Oper Res"},{"key":"56_CR24","doi-asserted-by":"crossref","unstructured":"Platzer A, Clarke EM (2009) Formal verification of curved flight collision avoidance maneuvers: a case study. In: International symposium on formal methods. Springer, Berlin, pp 547\u2013562\u200f","DOI":"10.1007\/978-3-642-05089-3_35"},{"key":"56_CR25","unstructured":"Rodin C, Jastram M, Butler M (2011) User\u2019s handbook"},{"issue":"1","key":"56_CR26","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10164-016-0484-6","volume":"35","author":"CV Schmidt","year":"2017","unstructured":"Schmidt CV et al (2017) First come, first served: the first-emerging queen monopolizes reproduction in the ant Cardiocondyla \u201cargyrotricha\u201d. J Ethol 35(1):21\u201327","journal-title":"J Ethol"},{"issue":"2","key":"56_CR27","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s10009-015-0400-3","volume":"19","author":"W Su","year":"2017","unstructured":"Su W, Abrial JR (2017) Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system. Int J Softw Tools Technol Transf 19(2):141\u2013166","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"4","key":"56_CR28","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/9.664154","volume":"43","author":"C Tomlin","year":"1998","unstructured":"Tomlin C, Pappas GJ, Sastry S (1998) Conflict resolution for air traffic management: a study in multiagent hybrid systems. IEEE Trans Autom Control 43(4):509\u2013521","journal-title":"IEEE Trans Autom Control"},{"key":"56_CR29","first-page":"657","volume":"484","author":"GL Vairaktarakis","year":"2007","unstructured":"Vairaktarakis GL, Aydinliyim T (2007) Benchmark schedules for subcontracted operations: decentralization inefficiencies that arise from competition and first-come-first-served processing. Decis Sci 484:657\u2013690","journal-title":"Decis Sci"},{"key":"56_CR30","unstructured":"Victor C, Mu\u00f1oz C (2005) Safety verification of the small aircraft transportation system concept of operations. In: AIAA 5th aviation, technology, integration, and operations conference (ATIO), Arlington, Virginia"},{"key":"56_CR31","doi-asserted-by":"crossref","unstructured":"Vistbakka I, Troubitsyna E (2018) Towards integrated modelling of dynamic access control with UML and Event-B. arXiv preprint arXiv:1805.05521","DOI":"10.4204\/EPTCS.271.8"},{"key":"56_CR32","doi-asserted-by":"crossref","unstructured":"Umeno S, Lynch N Safety verification of an aircraft landing protocol: a refinement approach. In: International workshop on hybrid systems: computation and control. Springer, Berlin, pp 557\u2013572 \u200f","DOI":"10.1007\/978-3-540-71493-4_43"},{"key":"56_CR33","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.ssci.2016.12.006","volume":"93","author":"Q Yang","year":"2017","unstructured":"Yang Q, Tian J, Zhao T (2017) Safety is an emergent property: illustrating functional resonance in Air Traffic Management with formal verification. Saf Sci 93:162\u2013177","journal-title":"Saf Sci"},{"issue":"4","key":"56_CR34","doi-asserted-by":"publisher","first-page":"3485","DOI":"10.1016\/j.asoc.2011.01.022","volume":"11","author":"SP Yu","year":"2011","unstructured":"Yu SP, Bin Cao X, Zhang J (2011) A real-time schedule method for aircraft landing scheduling problem based on cellular automation. Appl Soft Comput J 11(4):3485\u20133493","journal-title":"Appl Soft Comput J"},{"issue":"5","key":"56_CR35","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1186\/s40294-016-0014-y","volume":"4","author":"NA Zafar","year":"2016","unstructured":"Zafar NA (2016) Formal specification and analysis of take-off procedure using VDM-SL. Compl Adapt Syst Model 4(5):4","journal-title":"Compl Adapt Syst Model"}],"container-title":["Complex Adaptive Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s40294-018-0056-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s40294-018-0056-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s40294-018-0056-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T20:45:59Z","timestamp":1751834759000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1186\/s40294-018-0056-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,3]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["56"],"URL":"https:\/\/doi.org\/10.1186\/s40294-018-0056-4","relation":{},"ISSN":["2194-3206"],"issn-type":[{"value":"2194-3206","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9,3]]},"assertion":[{"value":"3 May 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 August 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 September 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"6"}}