CAV 2016
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration
Marco Gario, Alessandro Cimatti, Cristian Mattarei,
Stefano Tonetta, and Kristin Yvonne Rozier.
In the early stages of design, there are often many competing candidate solutions that differ in the assumptions and implementations of the components in use. Deciding which solution to adopt requires considering several trade-offs. Model checking represents a possible way of comparing such designs, however, it faces major challenges. For a large number of designs, building and validating so many models may be intractable.
During our collaboration with NASA, we faced the challenge of considering a design space with more than 20,000 designs for the NextGen air traffic control system. To deal with this problem, we introduce a compositional, modular, parameterized approach combining model checking with contract-based design to automatically generate large numbers of models from a possible set of components and their implementations. Our approach is fully automated, enabling the generation and validation of all target designs. The 1,620 designs that were most relevant to NASA were analyzed exhaustively. To deal with the massive amount of data generated, we apply novel data-analysis techniques, that enable a rich comparison of the designs, including safety aspects. Our results were validated by NASA system designers, and helped to identify novel as well as known problematic configurations.
Downloads:
