Formal Verification of Distributed Aircraft Controllers

As airspace becomes ever more crowded, air traffic management must reduce both space and time between aircraft to increase throughput, making on-board collision avoidance systems more important. These safety-critical systems must be extremely reliable and work properly under every circumstance. In tough scenarios where a large number of aircraft must execute a collision avoidance maneuver, a human pilot under stress is not necessarily able to understand the complexity of the distributed system and may not take the right course, especially if actions must be taken quickly. We consider a class of distributed collision avoidance controllers designed to work even in environments with arbitrarily many aircraft. We prove the controllers never allow aircraft to get too close to one another, even when new planes approach an in-progress avoidance maneuver. Because these safety guarantees always hold, the aircraft are protected against unexpected emergent behavior which simulation and testing may miss.