Loss of standard separation between aircraft can have hazardous consequences such as mid-air collisions and wake-vortex induced rolls. According to Air Route Traffic Control Center (ARTCC) reports, losses of standard separation rose to 10.6 % in 2017. Current air-traffic control (ATC) is dependent on human controllers who are prone to human errors. The system is not scalable and cannot be formally verified. Controller errors have been identified as 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.
With the integration of unmanned aircraft systems (UAS) for civilian applications, the density of aircraft in the National Airspace System (NAS) will increase significantly in the near future. Under such circumstances the concept of free-flight will become popular. It will, therefore, be imperative for pilots and UAS computers to have the ability to independently maintain standard separation between themselves.
The main goal of this project is to develop formally verifiable algorithms for strategic collision avoidance and air-traffic management. We envision smarter, formally verifiable, and more resilient air traffic management (ATM) protocols which will allow aircraft flying or planning to fly through a given airspace to cooperatively maintain standard separation between themselves.
- To develop formally verified algorithms for conflict-aware flight planning
- To develop formally verified protocols for cooperative flight planning and air-traffic management
Open Source Software/Formal Proofs:
- A conflict-aware flight planning algorithm (ATHENA)
- Progress in the Synod consensus protocol (TLA+, TLAPS)
- A distributed knowledge propagation protocol (TLA+, TLAPS)
- The following video shows the verification of our knowledge propagation protocol using TLAPS