Search papers, labs, and topics across Lattice.
This paper introduces a runtime verification framework designed to monitor spoken air traffic control procedures by analyzing controller-pilot exchanges, surveillance data, and onboard observations. The framework effectively parses radio communications into events linked to relevant entities and evaluates compliance with ICAO-derived obligations through formalized temporal formulas. Key results indicate an F1 score of 0.85 against human-annotated violations in real traffic and perfect accuracy in synthetic scenarios, demonstrating its potential to enhance safety in air traffic operations.
A runtime monitoring framework for air traffic control procedures achieves an impressive F1 score of 0.85, highlighting critical procedural violations that could prevent future accidents.
Air traffic control procedures are executed through spoken exchanges between controllers and pilots. These interactions are essential to the safety of air transportation: failures in their execution can create severe operational hazards, as evidenced by past fatal accidents. Assessing whether an instruction has been followed requires relating what was said to the aircraft concerned, its state, and the obligations that pilots must meet. We present a runtime verification framework that monitors such procedures by checking controller-pilot exchanges, surveillance data, and onboard observations. The framework parses radio communications into events linked to the entities they concern and merges them with surveillance and onboard observations into a time-stamped trace. The ICAO-derived obligations as formalized as temporal formulas with explicit time bounds and evaluated over execution traces. Every violation is reported along with the breached obligations and the observations that support the verdict. With real traffic, the complete pipeline reaches an F1 of 0.85 against blind human-annotated violations; in 1,495 synthetic situations derived from two public corpora, the monitor logic returns the expected verdict in every case. In two historical accidents reconstructed from official investigation reports, the monitor identifies the same procedural deviations documented by the investigators.
