Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems

Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems

Yang Zhao and Kristin Yvonne Rozier

2014

These pages contain further details of the experiments described in "Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems" by Yang Zhao and Kristin Yvonne Rozier.

Abstract:

Ensuring aircraft stay safely separated 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 a network of components providing multiple levels of separation assurance, including conflict detection and resolution. In our previous work, we conducted a formal study of this concept including specification, validation, and verification utilizing the NuSMV and CadenceSMV model checkers to ensure there are no potentially catastrophic design flaws remaining in the AAC design before the next stage of production. In this paper, we extend that work to include probabilistic model checking of the AAC system. We are motivated by the system designers' requirement to compare different design options to optimize the functional allocation of the AAC components. Probabilistic model checking provides quantitative measures for evaluating different design options, helping system designers to understand the impact of parameters in the model on a given critical safety requirement. We detail our approach to modeling and probabilistically analyzing this complex system consisting of a real-time algorithm, a logic protocol, and human factors. We utilize both Discrete Time Markov Chain (DTMC) and Continuous Time Markov Chain (CTMC) models to capture the important behaviors in the AAC components. The separation assurance algorithms, which are defined over specific time ranges, are modeled using a DTMC. The emergence of conflicts in an airspace sector and the reaction times of pilots, which can be simplified as Markov processes on continuous time, are modeled as a CTMC. Utilizing these two models, we calculate the probability of an unresolved conflict as a measure of safety and compare multiple design options.


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

Disclaimer: The files distributed on this page contain research prototype PRISM code published in the paper above. The files are compatible with PRISM version 4.0.3; we make no claims regarding compatibility with any other versions. Please feel free to email me concerning clarifications, bugs, or other corrections.


Run Script:

run_all.sh: Run from inside either nocheck/ or tsafecheck/ directory; runs all of the data points displayed in Figure 5.

PRISM Models for 'Checking' and 'No Checking' Designs:

Files for "no checking" scheme: Download nochecking.tgz

ar_tsafe.nm DTMC PRISM model of AAC separation assurance algorithms
ar_tsafe.pctl PCTL formula to check against the DTMC model in ar_tsafe.nm from Section II.A
process.py Check the value of AR res, TSAFE res, AR res time, and AR res time; use code below
const.sm Constants for CTMC initial state (generated from process.py)
csl.sm CSL formula to check against CTMC model from Section II.B (generated from process.py)
ctmc-const-val-template.sm Constant variables for the CTMC PRISM model of the complete AAC system
ctmc-check.sm
CTMC PRISM model of the complete AAC system


Files for "checking" scheme: Download tsafecheck.tgz

ar_tsafe.nm DTMC PRISM model of AAC separation assurance algorithms
ar_tsafe.pctl PCTL formula to check against the DTMC model in ar_tsafe.nm from Section II.A
ar_tsafe_const.nm Constant variables for DTMC model
process.py Check the value of AR res, TSAFE res, AR res time, and AR res time; use code below
const.sm
 input CTMC constants for initial states (generated from process.py)
ctmc-const-val.sm Constants variables in CTMC
csl.sm CSL formula to check against CTMC model from Section II.B (generated from process.py)
ctmc-check.sm
CTMC PRISM model of the complete AAC system

Kristin Yvonne Rozier 2014-06-17