The integration of Uncrewed Aircraft Systems (UAS) in the National Airspace System (NAS) for Urban Air Mobility (UAM) operations will create significant challenges for maintaining safe separation between the aircraft. The loss of safe separation can have hazardous consequences like near mid-air collisions (NMAC) and wake vortex induced rolls. Centralized approaches for air traffic management (ATM) that rely on human air traffic controllers are prone to human errors and awill not scale to the anticipated high-density air traffic. In fact, human errors have been identified as contributing factors in catasrophic incidents like the Gol Transportes Aéreos Flight 1907, the 2002 Überlingen mid-air collision, and the much recent collision between a Cessna and a Sabreliner.
The main goal of this project is to develop formally verifiable decentralized techniques for autonomous strategic coordination between aircraft for collision avoidance and ATM. We envision smarter and more resilient ATM standards and protocols which will allow aircraft flying or planning to fly through shared four-dimensional airspaces to cooperatively maintain standard separation between themselves without relying on centralized coordinators.
- To identify and address the challenges involved in decentralized coordination of multi-agent systems in asynchronous settings
- To use formal verification techniques to verify safety-critical correctness properties of the proposed solutions
Open Source Software/Formal Proofs:
- Our reusable Athena proof library for reasoning about distributed protocols
- Correctness proofs for a conflict-aware flight planning algorithm (ATHENA)
- Proof of eventual progress in the Synod consensus protocol (ATHENA)
- Correctness proofs for a distributed knowledge propagation protocol (TLA+, TLAPS)
- Proof of timely progress for the distributed knowledge propagation protocol (ATHENA)
- The following video shows the verification of our knowledge propagation protocol using TLAPS