Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics

We present the formally verified predicate and strategy used to independently evaluate the safety of the final version (Run 15) of the FAAs next-generation air-traffic collision avoidance system, ACAS X. This approach is a general one that can analyze simultaneous vertical and horizontal maneuvers issued by aircraft collision avoidance systems. The predicate is specialized to analyze sequences of vertical maneuvers, and in the horizontal dimension is modular, allowing it to be safely composed with separately analyzed horizontal dynamics. Unlike previous efforts, this approach enables analysis of aircraft that are turning, and accelerating non-deterministically. It can also analyze the safety of coordinated advisories, and encounters with more than two aircraft. We provide results on the safety evaluation of ACAS X coordinated collision avoidance on a subset of the system state space. This approach can also be used to establish the safety of vertical collision avoidance maneuvers for other systems with complex dynamics.