Modelling and Formal Verification of Safety-Critical Interactive System Using Capella and Event-B

By: Khaoula Bouba, Abderrahim Ait Wakrime, Yassine Ouhammou, Redouane Benaini

Abstract

The Arrival MANager (AMAN) system plays a crucial role in managing aircraft arrivals, optimizing landing sequences, and preventing congestion at airports. It aims to minimize delays and enhance airspace utilization. Safety breaches in the AMAN system can disrupt air traffic and compromise airport operations. To address these concerns, we model the AMAN system using Capella, a tool for Model-Based System Engineering (MBSE). Capella allows us to create two key models: Operational Analysis (OA) and System Analysis (SA). The OA captures the external environment and user needs, while the SA defines the internal system architecture to meet those needs. These models are interconnected to ensure the system's architecture aligns with its operational requirements. Next, we apply a Model-to-Model transformation to generate the Event-B model from the Capella input, formalizing the system's specifications. This enables the verification of safety and correctness. We use model-checking for formal verification, validating safety properties and ensuring the system's compliance with expected behaviors. The effectiveness of this approach is demonstrated through a realistic case study which is the AMAN system.

Keywords

Model-Based System Engineering, Capella/Arcadia, Formal methods, Event-B, Safety Critical Interactive System, Arrival Manager System

Cite as:

Khaoula Bouba, Abderrahim Ait Wakrime, Yassine Ouhammou, Redouane Benaini, “Modelling and Formal Verification of Safety-Critical Interactive System Using Capella and Event-B”, Journal of Object Technology, Volume 25, no. 2 ( 2026), pp. 2:7-36, doi:10.5381/jot.2026.25.2.a1.