SkyTrakx: A Toolkit for Simulation and Verification of Unmanned Air-Traffic Management Systems (Extended Version)
This addresses a domain-specific problem for unmanned aircraft systems traffic management, providing a toolkit for simulation and verification, but it is incremental as it builds on existing verification tools and concepts.
The paper tackles the lack of a framework for creating, manipulating, and reasoning about operation volumes (OVs) in unmanned air-traffic management by presenting SkyTrakx, a toolkit for simulation and verification, and shows its application in verifying protocols and computing OVs for heterogeneous vehicles, with experiments delineating trade-offs between performance and workload.
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.