Model Checking at Scale: Automated Air Traffic Control Design Space Exploration

dc.contributor.author Gario, Marco
dc.contributor.author Cimatti, Alessandro
dc.contributor.author Mattarei, Cristian
dc.contributor.author Tonetta, Stefano
dc.contributor.author Rozier, Kristin Yvonne
dc.contributor.author Rozier, Kristin
dc.contributor.department Aerospace Engineering
dc.contributor.department Computer Science
dc.contributor.department Electrical and Computer Engineering
dc.date 2019-08-11T17:24:10.000
dc.date.accessioned 2020-06-29T22:44:58Z
dc.date.available 2020-06-29T22:44:58Z
dc.date.copyright Fri Jan 01 00:00:00 UTC 2016
dc.date.embargo 2016-07-13
dc.date.issued 2016-07-13
dc.description.abstract <p>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.</p> <p>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.</p>
dc.description.comments <p>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) <em>Computer Aided Verification</em>. Part II. CAV 2016. Lecture Notes in Computer Science, vol 9780. The final publication is available at Springer via <a href="http://dx.doi.org/10.1007/978-3-319-41540-6_1" target="_blank">10.1007/978-3-319-41540-6_1</a>. Posted with permission.</p>
dc.format.mimetype application/pdf
dc.identifier archive/lib.dr.iastate.edu/aere_conf/33/
dc.identifier.articleid 1033
dc.identifier.contextkey 11299111
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath aere_conf/33
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/1911
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/aere_conf/33/2016_Rozier_ModelChecking.pdf|||Fri Jan 14 23:38:12 UTC 2022
dc.source.uri 10.1007/978-3-319-41540-6_1
dc.subject.disciplines Aerospace Engineering
dc.subject.disciplines Multi-Vehicle Systems and Air Traffic Control
dc.subject.disciplines Navigation, Guidance, Control and Dynamics
dc.subject.keywords Model Check
dc.subject.keywords Design Space
dc.subject.keywords Linear Temporal Logic
dc.subject.keywords Software Product Line
dc.subject.keywords Fault Tree
dc.title Model Checking at Scale: Automated Air Traffic Control Design Space Exploration
dc.type article
dc.type.genre conference
dspace.entity.type Publication
relation.isAuthorOfPublication 3c555e5b-8fd1-4c38-98c6-6a2449fab7cf
relation.isOrgUnitOfPublication 047b23ca-7bd7-4194-b084-c4181d33d95d
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456
relation.isOrgUnitOfPublication a75a044c-d11e-44cd-af4f-dab1d83339ff
File
Original bundle
Now showing 1 - 1 of 1
Name:
2016_Rozier_ModelChecking.pdf
Size:
578.06 KB
Format:
Adobe Portable Document Format
Description: