Modellazione formale e verifica runtime delle comunicazioni nel controllo del traffico aereo

Abstract

Le procedure di controllo del traffico aereo si svolgono attraverso scambi vocali tra controllori e piloti, la cui corretta esecuzione è essenziale per la sicurezza operativa. Valutarne la conformità richiede di associare le comunicazioni all’aeromobile a cui si riferiscono, al suo stato evolutivo e agli obblighi procedurali applicabili. Questa tesi sviluppa un framework di runtime verification per il monitoraggio di tali procedure, combinando comunicazioni controllore–pilota, dati di sorveglianza e osservazioni di bordo. Le trasmissioni radio vengono trascritte e analizzate per ricavarne eventi riferiti agli aeromobili e alle entità operative coinvolte, che vengono successivamente combinati con le osservazioni sullo stato degli aeromobili in una traccia temporizzata. Gli obblighi previsti dalla normativa ICAO sono formalizzati come formule di logica temporale, con scadenze e relazioni di precedenza esplicite, e valutati su tracce complete oppure progressivamente, all’arrivo di nuove osservazioni. Ogni violazione viene riportata insieme all’obbligo non rispettato e alle osservazioni che ne supportano il rilevamento. Per testare il funzionamento del sistema all’arrivo di nuove osservazioni, la tesi sviluppa inoltre un ambiente interattivo basato sul simulatore di traffico aereo BlueSky, che integra una postazione di controllo, agenti pilota che condividono un canale radio simulato e un componente anticollisione di bordo. Su traffico reale, la pipeline completa raggiunge un F1 di 0,85 rispetto alle violazioni annotate in cieco da annotatori umani; su 1.495 situazioni sintetiche derivate da due corpora pubblici, il monitor restituisce in ogni caso l’esito atteso. Le ricostruzioni degli incidenti di Überlingen e del volo Comair 5191 riproducono le deviazioni procedurali documentate dalle inchieste ufficiali.

Air traffic control procedures are carried out through spoken exchanges between controllers and pilots, whose correct execution is essential to operational safety. Assessing compliance requires relating what was said to the aircraft concerned, its evolving state, and the procedural obligations in force. This thesis develops a runtime verification framework that monitors such procedures by combining controller–pilot communications, surveillance data, and onboard observations. Radio transmissions are transcribed and parsed into events grounded in the aircraft and operational entities they concern, then merged with aircraft-state observations into a time-stamped trace. ICAO-derived obligations are formalized as temporal logic formulas with explicit deadlines and precedence relations, and evaluated over completed traces or incrementally as new observations arrive. Each violation is reported together with the breached obligation and the observations supporting the verdict. To exercise this incremental monitoring setting, the thesis also develops an interactive environment based on the BlueSky air traffic simulator, integrating a controller position, pilot agents sharing a simulated radio channel, and an onboard collision-avoidance component. On real traffic, the complete pipeline reaches an F1 of 0.85 against blind human-annotated violations; across 1,495 synthetic situations derived from two public corpora, the monitor returns the expected verdict in every case. Reconstructions of the Überlingen and Comair 5191 accidents reproduce the procedural deviations documented by official investigations.