Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System

To ensure the model checking results are meaningful, we have to ensure that both the model and specifications correctly reflect the intentions of the designers, thus we employ model validation and property debugging techniques.

We demonstrate the utility of enhancing LTL satisfiability checking by taking the fairness constraints of the system model into consideration. We argue that specification debugging in real applications deserves more attention in future research efforts, and the utility of a system formalization, model and specification debugging, and verification trilogy for model checking real systems under development. In this paper we assume there are no hardware failures or lost messages.