Formal analysis of air traffic management systems: the case of conflict resolution and recovery

New air traffic management concepts distribute the responsibility for traffic separation among the several actors of the aerospace system. As a consequence, these concepts move the safety risk from human controllers to the on-board software and hardware systems. One example of the new kind of distributed systems is air traffic conflict detection and resolution. Traditional methods for safety analysis such as human-in-the-loop simulations, testing, and flight experiments may not be sufficient in this highly distributed system: the set of possible scenarios is too large to have a reasonable coverage. This paper proposes a paradigm shift for the safety analysis of avionics systems where formal methods drive the development of critical systems. As a case study of this approach, we report the mechanical verification of an algorithm for air traffic conflict resolution and recovery.