SkyTrakx: A Toolkit for Simulation and Verification of Unmanned Air-Traffic Management Systems (Extended Version)

TL;DR

SkyTrakx is a comprehensive toolkit that enables simulation, verification, and analysis of unmanned aircraft traffic management scenarios using operation volumes, supporting heterogeneous vehicle types and formal property checking.

Contribution

It introduces SkyTrakx, a novel framework for creating, manipulating, and reasoning about operation volumes in UTM, integrating formal verification and reachability analysis for heterogeneous air vehicles.

Findings

SkyTrakx effectively verifies traffic protocols using Dafny and Dione.

It computes operation volumes for different vehicle types via reachability analysis.

The toolkit enables simulation of complex heterogeneous vehicle scenarios, assessing workload and response delays.

Abstract

The key concept for safe and efficient traffic management for Unmanned Aircraft Systems (UAS) is the notion of operation volume (OV). An OV is a 4-dimensional block of airspace and time, which can express an aircraft's intent, and can be used for planning, de-confliction, and traffic management. While there are several high-level simulators for UAS Traffic Management (UTM), we are lacking a framework for creating, manipulating, and reasoning about OVs for heterogeneous air vehicles. In this paper, we address this and present SkyTrakx -- a software toolkit for simulation and verification of UTM scenarios based on OVs. First, we illustrate a use case of SkyTrakx by presenting a specific air traffic coordination protocol. This protocol communicates OVs between participating aircraft and an airspace manager for traffic routing. We show how existing formal verification tools, Dafny and Dione, can assist in automatically checking key properties of the protocol. Second, we show how the OVs can be computed for heterogeneous air vehicles like quadcopters and fixed-wing aircraft using another verification technique, namely reachability analysis. Finally, we show that SkyTrakx can be used to simulate complex scenarios involving heterogeneous vehicles, for testing and performance evaluation in terms of workload and response delays analysis. Our experiments delineate the trade-off between performance and workload across different strategies for generating OVs.