Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering

Document Type

Conference Proceeding

Conference

28th International Conference on Computer Aided Verification (CAV 2016)

Publication Version

Accepted Manuscript

Link to Published Version

https://doi.org/10.1007/978-3-319-41540-6_1

Publication Date

2016

Journal or Book Title

Lecture Notes in Computer Science

Volume

9780

First Page

3

Last Page

22

DOI

10.1007/978-3-319-41540-6_1

Conference Date

July 17-23, 2016

City

Toronto, Ontario, CA

Abstract

Many possible solutions, differing in the assumptions and implementations of the components in use, are usually in competition during early design stages. Deciding which solution to adopt requires considering several trade-offs. Model checking represents a possible way of comparing such designs, however, when the number of designs is large, 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.

Comments

This is a manuscript of a proceeding published as Gario M., Cimatti A., Mattarei C., Tonetta S., Rozier K.Y. (2016) Model Checking at Scale: Automated Air Traffic Control Design Space Exploration. In: Chaudhuri S., Farzan A. (eds) Computer Aided Verification. CAV 2016. Lecture Notes in Computer Science, vol 9780. The final publication is available at Springer via https://doi.org/XX.XXXXX10.1007/978-3-319-41540-6_1. Posted with permission.

Copyright Owner

Springer International Publishing Switzerland

Language

en

File Format

application/pdf

Published Version

Share

Article Location

 
COinS