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

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 <span>SkyTrakx</span>a software toolkit for simulation and verification of UTM scenarios based on . First, we illustrate a use case of <span>SkyTrakx</span>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 <span>SkyTrakx</span>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 .

Acknowledgment {#acknowledgment .unnumbered}
==============

The authors were supported in part by research grants from the National Science Foundation (CyPhyHouse: 1629949 and FMitF: 1918531) and The Boeing Company. We thank John L. Olson, Aaron A. Mayne, and Michael R. Abraham from The Boeing Company for valuable technical discussions.

{'source': 'arXiv_out/2009'}