Formally Verified Decentralized Air Traffic Management

HTML5 Icon


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.

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!