Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics
ITP, pp. 336-353, 2017.
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 sy...More
Full Text (Upload PDF)
PPT (Upload PPT)