Yang Zhao and Kristin Yvonne Rozier
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.
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.
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|
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.
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 runThe 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.