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

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.

Original document

The different versions of the original document can be found in:

• https://lib.dr.iastate.edu/cgi/viewcontent.cgi?article=1033&context=aere_conf

• http://link.springer.com/content/pdf/10.1007/978-3-319-41540-6_1,

http://dx.doi.org/10.1007/978-3-319-41540-6_1 under the license http://www.springer.com/tdm

• https://link.springer.com/chapter/10.1007/978-3-319-41540-6_1,

https://dblp.uni-trier.de/db/conf/cav/cav2016-2.html#GarioCMTR16,

https://lib.dr.iastate.edu/aere_conf/33,

https://lib.dr.iastate.edu/cgi/viewcontent.cgi?article=1033&context=aere_conf,

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

https://rd.springer.com/chapter/10.1007%2F978-3-319-41540-6_1,

https://works.bepress.com/kristin-yvonne-rozier/14,

https://academic.microsoft.com/#/detail/2493561771