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

Abstract

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 NuSMV and perform model validation by checking
against LTL/CTL specifications 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.