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

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

Yang Zhao and Kristin Yvonne Rozier

2012-2013

These pages contain further details of the experiments described in "Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System" by Yang Zhao and Kristin Yvonne Rozier.

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 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. Our contributions include: a derivation of the operational procedure of the AAC in formal semantics that can be used for both model checking and as a prototype for implementation; an adaptation of the state-of-the-art in specification debugging and model abstraction techniques for efficient design-time feedback, verification, and validation for both the system and specifications; and an analysis revealing unexpected emergent behaviors in the system not found by other verification efforts, delivering counterexamples which pinpoint their locations. We include examples of the models both before and after system designers changed the design in response to our counterexamples to ensure compliance with safety requirements.

Our models and specifications can be checked using the symbolic model checker NuSMV, which is free and open source and can be downloaded here. The User Manual can be found here.

Equivalent models and specifications with the syntax slightly modified to enable checking using the symbolic model checker CadenceSMV are also provided. We used the precompiled binary available here. The User Manual can be found here and a tutorial can be found here (or here).

Disclaimer: The files distributed on this page contain research prototype NuSMV code published in the paper above. The files are compatible with NuSMV version 2.5.x and the CadenceSMV compiled binary smv.10-11-02p46.unknown_Linux_2.4.2-2; we make no claims regarding compatibility with any other versions. Please feel free to email me concerning clarifications, bugs, or other corrections.


AAC Complete Logic Model

The NuSMV and CadenceSMV logic models of the high-level AAC architecture, including all specifications for both System Design Validation and System Requirements Verification can be found here:

Original NuSMV Complete Model with 3 Planes AAC_NuSMV_3.smv
NuSMV Complete Model with 3 Planes, changed to fix LTL-8 AAC_NuSMV_3fix.smv
Original CadenceSMV Complete Model with 3 Planes AAC_CadenceSMV_3.smv
CadenceSMV Complete Model with 3 Planes, changed to fix LTL-8 AAC_CadenceSMV_3fix.smv

This full-detail model contains 97 Boolean variables. The time required to verify all specifications is more than 10 hours using NuSMV and over 1 hour using Cadence SMV on an Intel Xeon 2.53GHz workstation running 64-bit CentOS Linux (kernel version 2.6.18) with 36GB RAM.

Though we could not check larger models with available computing resources, we also created models with 4 planes. They can be found here:

Original NuSMV Complete Model with 4 Planes AAC_NuSMV_4.smv
NuSMV Complete Model with 4 Planes, changed to fix LTL-8 AAC_NuSMV_4fix.smv
Original CadenceSMV Complete Model with 4 Planes AAC_CadenceSMV_4.smv
CadenceSMV Complete Model with 4 Planes, changed to fix LTL-8 AAC_CadenceSMV_4fix.smv


AAC Abstract Model

The abstract model, which we created to enable fast, design-phase testing, can be found for both NuSMV and CadenceSMV here.

NuSMV Abstract Model with 3 Planes AAC_NuSMV_3abs.smv
CadenceSMV Abstract Model with 3 Planes AAC_CadenceSMV_3abs.smv
NuSMV Abstract Model with 4 Planes AAC_NuSMV_4abs.smv
CadenceSMV Abstract Model with 4 Planes AAC_CadenceSMV_4abs.smv

The set of possible executions in the abstract model is a strict super-set of the possible executions in the original model, above.

The abstract model with 3 planes takes only a little more than a minute to verify all properties for NuSMV and a few seconds for Cadence SMV. The abstract model with 4 planes requires minimally longer to check than with 3 planes. It is important to note that for the 4-plane models, only the abstract models (and not the complete models) could be checked with our available computing resources.


AAC Verification Commands

For NuSMV, here is the command file cmd-file we used, it looks like: 

set dynamic_reorder                    -- enables dynamic reordering of BDD variables in the CUDD package
read_model -i MODEL.smv                -- read the logic model in to NuSMV, replace MODEL.smv the file name of the model you want to verify.
go                                     -- initialize the system for the verification
print_bdd_stats                        -- print out the BDD statistics and parameters
check_ltlspec -P "property-name"       -- perform LTL model checking, replace property-name with the LTL property name (written as "LTLSPEC NAME property-name :=" in our model) you want to verify. 
check_ctlspec -P "property-name"       -- perform CTL model checking, replace property-name with the CTL property name (written as "CTLSPEC NAME property-name :=" in our model) you want to verify. 
time                                   -- provides a simple CPU elapsed time value
print_bdd_stats                        -- print out the BDD statistics and parameters
quit                                   -- end of verification run
The command to run NuSMV with this script is: 
% NuSMV -source cmd-file

For Cadence SMV, use the command:

% smv -sift -together MODEL.smv

to check all of the properties.


Kristin Yvonne Rozier 2013-03-22