Formally Verified Conflict-Aware Flight Planning

HTML5 Icon


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.

This project was conceived at the Worldwide Computing Laboratory (WCL), Rensselaer Polytechnic Institute, as a child project of the PILOTS programming language.



Open Source Software/Formal Proofs:

Comments/suggestions/patches are welcome!