Before revision:  In this paper, we explore applying rigorous formal reasoning on building and analyzing UTM protocols to (1) help provide high assurance on UTM protocols and (2) discover the strength and weaknesses of existing formal techniques. We propose the first mathematical formalization of FAA's notion of operation volumes that express aircraft intent in terms of 4D blocks of airspace and associated real-time deadlines. We present an executable prototype coordination protocolusing operation volumes, involving participating aircraft and an airspace manager . Next, we show how to use an ensemble of existing simulation and formal verification tools to analyze the protocol including (1)
After revision:  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 . Next, we show how to use an ensemble of existing simulation and formal verification tools to analyze the protocol including (1)