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.
After revision:  In this paper, we propose the first formalization of FAA's Concept of Operations for UTM report. In this paper, we explore applying rigorous formal reasoning on building and analyzing traffic management protocols and systems.