A formal approach to UAV safety and security: from modeling to verification

Urban Air Mobility (UAM) is emerging as a transformative paradigm in transportation, leveraging aerial vehicles such as electric Vertical Take-Off and Landing (eVTOL) aircraft and autonomous drones to address urban congestion and environmental challenges. UAM promises scalable, efficient, and sustainable mobility solutions across domains including passenger transport, logistics, emergency response, and infrastructure monitoring. However, its deployment introduces complex challenges in safety, security, coordination, reliability, and regulatory compliance. This thesis investigates the role of formal methods -- rigorous mathematical techniques for system specification, verification, and synthesis -- in addressing key operational challenges in UAM. Specifically, it explores how formal methods can ensure reliable communication networks, safe scheduling and routing, and strategic deconfliction of aerial vehicles. The work emphasizes the use of Answer Set Programming (ASP), a declarative programming paradigm well-suited for modelling and solving combinatorial problems in dynamic and heterogeneous environments. The research methodology leverages ASP to bridge the gap between raw operational data and formal system verification. The thesis provides three primary contributions. First, Security through Pattern Mining, introducing MASS-CSP, a declarative framework for mining contrast sequential patterns. This tool identifies temporally correlated cyber threats and anomalies in UAM communication networks by encoding complex pattern preferences as logical constraints. Second, Security through Specification Mining, developing ASPecMINE, an ASP-based approach to mine LTL properties from system logs. This enables the derivation of formal behavioural models, allowing for the detection of deviations from safety and liveness protocols. Third, Safety through Strategic Deconfliction, implementing STRADA, which applies ASP to the strategic deconfliction problem. This approach synthesizes conflict-free, time-synchronized flight routes, ensuring separation constraints are met during the mission planning phase. Collectively, these contributions establish a unified research agenda where declarative logic and ASP serves as a versatile formalism for both diagnostic security (mining patterns and specifications) and proactive safety (conflict resolution). The results demonstrate that formal methods and in particular ASP not only enhance the robustness of UAM architectures but also provide the scalability required for dense urban air traffic.

La mobilità aerea urbana (UAM) si sta affermando come paradigma trasformativo nei trasporti, sfruttando veicoli aerei come i velivoli elettrici a decollo e atterraggio verticale (eVTOL) e i droni autonomi per affrontare la congestione urbana e le sfide ambientali. L'UAM promette soluzioni di mobilità scalabili, efficienti e sostenibili in diversi settori, tra cui il trasporto passeggeri, la logistica, la risposta alle emergenze e il monitoraggio delle infrastrutture. Tuttavia, la sua implementazione introduce sfide complesse in termini di sicurezza, protezione, coordinamento, affidabilità e conformità normativa. Questa tesi indaga il ruolo dei metodi formali, ovvero tecniche matematiche rigorose per la specifica, la verifica e la sintesi dei sistemi, nell'affrontare le principali sfide operative nell'UAM. In particolare, esplora come i metodi formali possano garantire reti di comunicazione affidabili, pianificazione e routing sicuri e la deconflittualità strategica dei veicoli aerei. Il lavoro enfatizza l'uso dell'Answer Set Programming (ASP), un paradigma di programmazione dichiarativa adatto alla modellazione e alla risoluzione di problemi combinatori in ambienti dinamici ed eterogenei. La metodologia di ricerca sfrutta l'ASP per colmare il divario tra dati operativi grezzi e verifica formale del sistema. La tesi fornisce tre contributi principali. In primo luogo, la sicurezza attraverso il Pattern Mining, con l'introduzione di MASS-CSP, un framework dichiarativo per l'analisi di pattern sequenziali di contrasto. Questo strumento identifica minacce informatiche e anomalie correlate temporalmente nelle reti di comunicazione UAM codificando complesse preferenze di pattern come vincoli logici. In secondo luogo, la sicurezza attraverso lo Specification Mining, con lo sviluppo di ASPecMINE, un approccio basato su ASP per l'analisi di proprietà LTL dai log di sistema. Ciò consente la derivazione di modelli comportamentali formali, consentendo il rilevamento di deviazioni dai protocolli di sicurezza e di vitalità. In terzo luogo, la sicurezza attraverso la deconflittualità strategica, con l'implementazione di STRADA, che applica ASP al problema della deconflittualità strategica. Questo approccio sintetizza rotte di volo sincronizzate e prive di conflitti, garantendo il rispetto dei vincoli di separazione durante la fase di pianificazione della missione. Nel complesso, questi contributi stabiliscono un programma di ricerca unificato in cui la logica dichiarativa e ASP fungono da formalismo versatile sia per la sicurezza diagnostica (analisi di pattern e specifiche) sia per la sicurezza proattiva (risoluzione dei conflitti). I risultati dimostrano che i metodi formali e in particolare ASP non solo migliorano la robustezza delle architetture UAM, ma forniscono anche la scalabilità richiesta per un denso traffico aereo urbano.