A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System

By Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora C. Schmidt, Erik Zawadzki, André Platzer. 2015

84 citations recorded by the source corpus.

The Next-Generation Airborne Collision Avoidance System ACASi¾?X is intended to be installed on all large aircraft to give advice to pilots and prevent mid-air collisions with other aircraft. It is currently being developed by the Federal Aviation Administration FAA. In this paper we determine the geometric configurations under which the advice given by ACAS X is safe under a precise set of assumptions and formally verify these configurations using hybrid systems theorem proving techniques. We conduct an initial examination of the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal, hybrid approaches are helping ensure the safety of ACAS X. Our approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.

Subfields: Aerospace Engineering, Automotive Engineering, Safety, Risk, Reliability and Quality, Safety, Robustness & Interpretability, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Aerospace Engineering

In Automotive Engineering

In Safety, Risk, Reliability and Quality

Jacob Steinhardt

In Safety, Robustness & Interpretability

In Program Analysis & Verification

Citations in the corpus

Concrete Problems in AI Safety (2016, background): “Illustrative of this work is an impressive and successful effort to formally verify the entire federal aircraft collision avoidance system [73, 90].”
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017, methodology): “It will be interesting to combine our technique with that of [12], in order to verify that following the advisories provided by the DNNs indeed leads to collision avoidance.”
Towards Proving the Adversarial Robustness of Deep Neural Networks (2017, methodology): “Specifically, we plan to explore the integration of Reluplex with reachability analysis techniques, for both the offline [11] and online [1] variants.”
Differential Adaptive Stress Testing of Airborne Collision Avoidance Systems (2018, unknown): “Other studies have used hybrid systems theorem proving (HSTP), which models encounters as hybrid systems with idealized advisories and continuous dynamics then formally proves whether the system always avoids collision or whether a collision is possible [6][7].”