FMCAD 2015
PhD candidate Cristian Mattarei gave a wonderful presentation of our work on “Comparing Different Functional Allocations in Automated Air Traffic Control Design” by Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, and Kristin Y. Rozier today at Formal Methods in Computer-Aided Design (FMCAD) 2015 at the University of Texas at Austin. Our paper stems from a fruitful collaboration with the Embedded Systems Laboratory at the Fondazione Bruno Kessler (FBK) in Trento, Italy.
The slides are available here.
FMCAD 2015
ABSTRACT:
In the early phases of the design of safety-critical
systems, we need the ability to analyze the safety of different
design solutions, comparing how different functional allocations
impact the overall reliability of the system. To achieve this
goal, we can apply formal techniques ranging from model
checking to model-based fault-tree analysis. Using the results
of the verification and safety analysis, we can compare different
solutions and provide the domain experts with information on
the strengths and weaknesses of each solution.
In this paper, we consider NASA’s early designs and functional
allocation hypotheses for the next air traffic control system for
the United States. In particular, we consider how the allocation of
separation assurance capabilities and the required communication
between agents affects the safety of the overall system. Due
to the high level of details, we need to abstract the domain while
retaining all of the key properties of NASA’s designs. We present
the modeling approach and verification process that we adopted.
Finally, we discuss the results of the analysis when comparing
different configurations including both new, self-separating and
traditional, ground-separated aircraft.