Formal modeling of a complex adaptive air traffic control system
Open accessAbstract
Abstract 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’ 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.
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
CAS are proactive in choosing between available actions by looking ahead to anticipate future consequences.
“CAS are not only reactive, but also proactive in choosing between available actions by noncommittally looking ahead to anticipate future consequences, for example ensuring safety in air traffic control systems (Jarrar & Balouki, 2018).”
From Interactive digital narrative (IDN)—new ways to represent complexity and facilitate digitally empowered citizens (2022) · cites this paper as Jarrar & Balouki, 2018
The SAF-2 section says the proposed air traffic control system can predict whether aircraft deadlines can be met and notify a controller; the first-refinement section describes a choice between proceeding with landing and redirecting an aircraft. These passages support anticipation in this specific system, but not the broader claim that CAS generally choose actions by noncommittally looking ahead at their consequences. (LLM, conf=0.84)
Experimental — accuracy not yet measured
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Cites
No references could be resolved yet.
Research works printed but not linked: 25
- Abrial J-R (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, New York
- 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-466
- 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-485
- 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
- Cansell D, Méry D, Rehm J (2007) Time constraint patterns for Event B development. In: International conference of B users. Springer, Berlin, pp 140-154
- Clarke EM, Wing JM (1996) Formal methods: state of the art and future directions. ACM Comput Surv (CSUR) 28(4):626-643
- Dominique M, Neeraj KS (2011) EB2J: code generation from Event-B to Java, SBMF. IN: Brazilian symposium on formal methods, São Paulo, Brazil
- 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-159 Fact Sheet-FAA & NTSB's "Most Wanted" Recommendations (2010) https ://www.faa.gov/news/fact_sheet s/news_story .cfm?newsI d=11186 . Accessed 20 May 2018
- Hoang TS, Kuruma H, Basin D, Abrial JR (2009) Developing topology discovery in Event-B. Sci Comput Program 74(11-12):879-899
- Jarrar A et al (2017) Modeling aircraft landing scheduling in Event B. In: International conference on information technol- ogy and communication systems. Springer, Berlin, pp 127-142
- Jarrar A, Balouki Y (2018) Formal reasoning for air traffic control system using Event-B method. In: International confer- ence on computational science and its applications. Springer, Cham, pp 241-252
- Jarrar A, Balouki Y, Gadi T (2017) Formal specification of QoS negotiation in ODP system. Int J Elec Comput Eng 7(4):2045
- Lecomte T, Servat T, Pouzancre G (2007) Formal methods in safety-critical railway systems. In: 10th Brasilian symposium on formal methods, pp 29-31
- 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 .234-404
- 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-1834
- Pinol H, Beasley JE (2006) Scatter search and bionomic algorithms for the aircraft landing problem. Eur J Oper Res 171(2):439-462
- Platzer A, Clarke EM (2009) Formal verification of curved flight collision avoidance maneuvers: a case study. In: Interna- tional symposium on formal methods. Springer, Berlin, pp 265-745
- Rodin C, Jastram M, Butler M (2011) User's handbook Schmidt CV et al (2017) First come, first served: the first-emerging queen monopolizes reproduction in the ant Cardio- condyla "argyrotricha". J Ethol 35(1):21-27
- 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-166
- 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-521
- Victor C, Muñoz 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
- Vistbakka I, Troubitsyna E (2018) Towards integrated modelling of dynamic access control with UML and Event-B. arXiv preprint arXiv :1805.05521 · arXiv
- 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-572
- 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-3493
- Zafar NA (2016) Formal specification and analysis of take-off procedure using VDM-SL. Compl Adapt Syst Model 4(5):4
Cited by
Sorted by citations
Koenitz, H., Barbara, J., & Eladhari, M. P. (2022) · New Review of Hypermedia and Multimedia · doi:10.1080/13614568.2023.2181503 · Cited by 28 · see citing works
“CAS are not only reactive, but also proactive in choosing between available actions by noncommittally looking ahead to anticipate future consequences, for example ensuring safety in air tra ffi c control systems (Jarrar & Balouki, 2018).”
Background
- Authors
- Jarrar, A., & Balouki, Y.
- Affiliations
- Université Hassan 1er (MA)
- Corresponding author
- Balouki, Youssef
- Venue
- Complex Adaptive Systems Modeling
- Published
- 2018-09-03
- Volume
- 6
- Issue
- 1
- ISSN
- 2194-3206 (ISSN-L)
- OpenAlex
- W2891012439
- Cited by
- 16
- References
- 0
- Citations by year
- 2026: 2 · 2023: 3 · 2022: 4 · 2021: 1 · 2020: 2 · 2019: 4
- FWCI
- 1.31
- Type
- journal article
- Language
- en
- Open access
- hybrid
- doi.org
- Locations
- Complex Adaptive Systems Modeling (publishedVersion, cc-by)
- DOAJ (DOAJ: Directory of Open Access Journals) (submittedVersion)
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Engineering › Aerospace Engineering › Air Traffic Management and Optimization
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Petri Nets in System Modeling
- Keywords
- air traffic control, Event-B, formal modeling, refinement, model correctness, air traffic management, critical systems, software assurance
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
