  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.
