Formally Verified Next-generation Airborne Collision Avoidance Games in ACAS X
Abstract
The design of aircraft collision avoidance algorithms is a subtle but important challenge that merits the need for provable safety guarantees. Obtaining such guarantees is nontrivial given the unpredictability of the interplay of the intruder aircraft decisions, the ownship pilot reactions, and the subtlety of the continuous motion dynamics of aircraft. Existing collision avoidance systems, such as TCAS and the Next-Generation Airborne Collision Avoidance System ACAS X, have been analyzed assuming severe restrictions on the intruder’s flight maneuvers, limiting their safety guarantees in real-world scenarios where the intruder may change its course.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 29, 2022
- Source ID
- 10.1145/3544970
Entities
People
- André Platzer
- Rachel Cleaveland
- Stefan Mitsch
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University