Application of Multi-architecture Modeling Method in Air Traffic Management System Design

Abstract

The increasing complexity of Air Traffic Management (ATM) systems calls for systematic methods that can support forward architecture design and early verification. This paper proposes a model-based systems engineering (MBSE) approach that integrates a multi-architecture modeling language, developed from the GOPPRRE meta-metamodel, with satisfiability modulo theory (SMT) for static verification. The proposed method provides two key contributions: a unified KARMA-based framework that organizes strategic, operational, service, and resource perspectives into a consistent multi-domain architecture, and an embedded SMT mechanism that enables automated detection of inconsistencies and constraint violations at the early design stage. A case study illustrates the construction of a tailored UAF-based ATM architecture, where SMT checking validates capability coverage, communication integrity, and logical consistency. These findings demonstrate that integrating multi-architecture modeling with early-stage formal verification not only enhances model consistency but also provides a repeatable pathway for life cycle management – from conceptual design through system validation – thereby supporting continuous evolution of ATM architectures within a model-based development environment. Quantitative results show that the method supports architecture development with more than 350 defined meta-elements and achieves static verification in a few seconds. The integration of multi-architecture modeling with formal verification enhances traceability, reduces design rework, and strengthens the robustness of ATM system development.

Keywords

Air traffic management system / MBSE / KARMA language / multi-architecture modeling / SMT verification

References

[1] Barrett C, Tinelli C. Satisfiability modulo theories. Handbook of Model Checking, 2018, Switzerland, Springer International Publishing305343

[2] Bi W, Wang W, Zhang A, Wang Y. Extending modelbased systems engineering into integrated platform designed for civil aircraft development. Journal of Aerospace Technology and Management, 2021, 13: e2321

[3] Boggero L, Lefebvre T, Vankan J, Beijer B, Saluzzi V, Nagel B. The AGILE 4.0 MBSE-MDAO development framework: Overview and assessment. 33rd Congress of the International Council of the Aeronautical Sciences, 2022September 4–9, 2022

[4] Chaudemar J C, Saqui-Sannes P. MBSE and MDAO for early validation of design decisions: A bibliography survey. 2021 IEEE International Systems Conference (SysCon), 2021Virtual event

[5] Chen J, Chen Y, Hu Z, Lu J, Zheng X, Zhang H, Kiritsis D. A semantic ontology-based approach to support model-based systems engineering design for an aircraft prognostic health management system. Frontiers in Manufacturing Technology, 2022, 2: 886518

[6] Ciampa P D, Nagel B. Agile paradigm: The next generation collaborative MDO for the development of aeronautical systems. Progress in Aerospace Sciences, 2020, 119: 100643

[7] Cook D, Schindel W D. Utilizing MBSE patterns to accelerate system verification. INSIGHT, 2017, 20(1): 32-41

[8] Cordeiro L C, de Lima Filho E B. SMT-based context-bounded model checking for embedded systems: Challenges and future trends. SIGSOFT Software Engineering Notes, 2016, 41(3): 1-6

[9] De Moura L, Bjørner N. Satisfiability modulo theories: Introduction and applications. Communications of the ACM, 2011, 54(9): 69-77

[10] Dandashi F, Hause M C. UAF for system of systems modeling. 2015 10th System of Systems Engineering Conference (SoSE), 2015May 17–20, 2015

[11] Ding J, Reniers M, Lu J, Wang G, Feng L, Kiritsis D. Integration of modeling and verification for system model based on KARMA language. 18th ACM SIGPLAN International Workshop on Domain-Specific Modeling (DSM 2021), 2021October 18, 2021

[12] Flink J, Mischke R, Schaffert K, Schneider D, Weinert A. Orchestrating tool chains for model-based systems engineering with RCE. 2022 IEEE Aerospace Conference (AERO), 2022March 05–12, 2022

[13] Forman B. The political process in systems architecture design. INCOSE International Symposium, 1993, 3(1): 92-97

[14] Forman B. The political process and systems architecting. The Art of Systems Architecting, 2025, USA, CRC Press426-437

[15] Gómez-Rodríguez Á, Turkoglu C, Cuerno-Rejado C. A systematic approach towards the integration of initial airworthiness regulatory requirements in RPAS conceptual design methodologies. Aerospace, 2024, 11(9): 735

[16] Gurfinkel A, Shoham S, Meshman Y. SMT-based verification of parameterized systems. 24th ACM SIGSOFT International Symposium on Foundations of Software Engineerin (FSE 2016), 2016November 13–18, 2016

[17] Hackenberg D L. AAM for FAA/NASA research roundtable (No. AFRC-E-DAA-TN78388), 2020

[18] Hause M, Bleakley G, Morkevicius A. Technology update on the unified architecture framework (UAF). INSIGHT, 2017, 20(2): 71-78

[19] Heydari S A. Model-based systems engineering (MBSE) for complex engineering projects. Management Strategies and Engineering Sciences, 2023, 5(2): 22-31

[20] Krupa G P. Application of agile model-based systems engineering in aircraft conceptual design. The Aeronautical Journal, 2019, 123(1268): 1561-1601

[21] Li S, Deng K. UAF-based air transportation cooperative information SoS modeling under ‘Belt and Road Initiative’. 2022 IEEE 6th Information Technology and Mechatronics Engineering Conference (ITOEC), 2022March 4–6, 2022

[22] Lu J, Wang G, Ma J, Kiritsis D, Zhang H, Törngren M. General modeling language to support model-based systems engineering formalisms (Part 1). INCOSE International Symposium, 2020, 30(1): 323-338

[23] Maheshwari A. Industrial adoption of model-based systems engineering: Challenges and strategies, 2015

[24] Mehta A, Alaiashy O, Kumar P, Tamilinian V, Besong S, Balpande S, Verma S, Dhingra K. Advancing model-based systems engineering in biomedical and aerospace research: A comprehensive review and future directions. Journal of Knowledge Learning and Science Technology, 2024, 3(4): 133-147

[25] Sun Y, Smith H. Review and prospect of supersonic business jet design. Progress in Aerospace Sciences, 2017, 90: 12-38

[26] Wang J, Deng Y. Incremental modeling and verification of flexible manufacturing systems. Journal of Intelligent Manufacturing, 1999, 10(6): 485-502

[27] Wang H, Wang G, Lu J, Ma C. Ontology supporting model-based systems engineering based on a GOPPRR approach. New Knowledge in Information Systems and Technologies, 2019, Switzerland, Springer International Publishing426436

[28] Wymore A W. Model-based Systems Engineering, 2018, USA, CRC Press

[29] Zhang L, Ye F, Xie K, Gu P, Wang X, Laili Y, Zhao C, Zhang X, Chen M, Lin T, Chen Z. An integrated intelligent modeling and simulation language for modelbased systems engineering. Journal of Industrial Information Integration, 2022, 28: 100347

[30] Zheng X, Hu X, Lu J, Arista R, Lentes J, Kiritsis D. An aircraft assembly process formalism and verification method based on semantic modeling and MBSE. Advanced Engineering Informatics, 2024, 60: 102412

RIGHTS & PERMISSIONS

Systems Engineering Society of China and Springer-Verlag GmbH Germany

Just Accepted

This article has successfully passed peer review and final editorial review, and will soon enter typesetting, proofreading and other publishing processes. The currently displayed version is the accepted final manuscript. The officially published version will be updated with format, DOI and citation information upon launch. We recommend that you pay attention to subsequent journal notifications and preferentially cite the officially published version. Thank you for your support and cooperation.