Before revision:  In this paper, we propose the first formalization of FAA's Concept of Operations for UTM for building and analyzing traffic management protocols and systems. We formalize FAA's notion of operation volumes (OVs) that express aircraft intent in terms of 4D blocks of airspace and associated real-time deadlines.
After revision:  In this paper, we propose the first formalization of FAA's Concept of Operations for UTM for 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 (OVs) that express aircraft intent in terms of 4D blocks of airspace and associated real-time deadlines.