Background:

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 is a part of the ASSURE research program at the Worldwide Computing Laboratory (WCL), Rensselaer Polytechnic Institute.

Goals:

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

Publications:

WCL publications on air traffic management

Open Source Software/Formal Proofs:

Comments/suggestions/patches are welcome!

Videos/Demo:

The following video shows the verification of our knowledge propagation protocol using TLAPS