Formal specification and verification of a coordination protocol for an automated air traffic control system

• Formalize the high-level operational concept and perform model validation.
• Write formal specifications and use model checking for system verification.
• Employ LTL specification debugging to ensure correctness of formal specifications.
• Analyze two counterexamples revealing unexpected emergent behaviors that triggered design changes by system engineers to meet safety standards.
• Illuminate the application of formal methods in real safety-critical system development.

Safe separation between aircraft is the primary consideration in air traffic control. To achieve the required level of assurance for this safety-critical application, the Automated Airspace Concept (AAC) proposes three levels of conflict detection and resolution. Recently, a high-level operational concept was proposed to define the cooperation between components in the AAC. However, the proposed coordination protocol has not been formally studied. We use formal verification techniques to ensure there are no potentially catastrophic design flaws remaining in the AAC design before the next stage of production.We formalize the high-level operational concept, which was previously described only in natural language, in both NuSMV and CadenceSMV, and perform model validation by checking against temporal logic specifications in LTL and CTL that we derive from the system description. We write LTL specifications describing safe system operations and use model checking for system verification. We employ specification debugging to ensure correctness of both sets of formal specifications and model abstraction to reduce model checking time and enable fast, design-time checking. We analyze two counterexamples revealing unexpected emergent behaviors in the operational concept that triggered design changes by system engineers to meet safety standards. Our experience report illuminates the application of formal methods in real safety-critical system development by detailing a complete end-to-end design-time verification process including all models and specifications.