{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T09:10:41Z","timestamp":1774775441379,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415390","type":"print"},{"value":"9783319415406","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41540-6_1","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:07Z","timestamp":1468316047000},"page":"3-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Model Checking at Scale: Automated Air Traffic Control Design Space Exploration"],"prefix":"10.1007","author":[{"given":"Marco","family":"Gario","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]},{"given":"Cristian","family":"Mattarei","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]},{"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"1_CR1","unstructured":"Eric & Wendy Schmidt Data Science for Social Good, University of Chicago. \n                      http:\/\/dssg.uchicago.edu\/"},{"key":"1_CR2","unstructured":"NASA airspace operations and safety program. \n                      http:\/\/www.aeronautics.nasa.gov\/programs-aosp.htm"},{"key":"1_CR3","unstructured":"Nasa nextgen-airspace. \n                      http:\/\/www.hq.nasa.gov\/office\/aero\/asp\/airspace\/"},{"key":"1_CR4","unstructured":"Project webpage: Formal methods for automated airspace concepts. \n                      https:\/\/es-static.fbk.eu\/projects\/nasa-aac"},{"key":"1_CR5","unstructured":"NextGen, May 2016. \n                      https:\/\/www.faa.gov\/nextgen\/"},{"issue":"1","key":"1_CR6","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M Abadi","year":"1993","unstructured":"Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73\u2013132 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR7","unstructured":"ARP4754A guidelines for development of civil aircraft and systems. In: SAE, December 2010"},{"key":"1_CR8","unstructured":"ARP4761 guidelines and methods for conducting the safety assessment process on civil airborne systems and equipment. In: SAE, December 1996"},{"issue":"4","key":"1_CR9","doi-asserted-by":"publisher","first-page":"1023","DOI":"10.2514\/1.26311","volume":"30","author":"C Bauer","year":"2007","unstructured":"Bauer, C., Lagadec, K., B\u00e8s, C., Mongeau, M.: Flight control system architecture optimization for fly-by-wire airliners. J. Guidance Control Dyn. 30(4), 1023\u20131029 (2007)","journal-title":"J. Guidance Control Dyn."},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-662-49674-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Bittner","year":"2016","unstructured":"Bittner, B., Bozzano, M., Cavada, R., Cimatti, A., Gario, M., Griggio, A., Mattarei, C., Micheli, A., Zampedri, G.: The xSAP safety analysis platform. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 533\u2013539. Springer, Heidelberg (2016)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1007\/978-3-319-21690-4_41","volume-title":"Computer Aided Verification","author":"M Bozzano","year":"2015","unstructured":"Bozzano, M., Cimatti, A., Griggio, A., Mattarei, C.: Efficient anytime techniques for model-based safety analysis. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 603\u2013621. Springer, Heidelberg (2015)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Cimatti, A., Mattarei, C.: Automated analysis of reliability architectures. In: 18th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 198\u2013207. IEEE, July 2013","DOI":"10.1109\/ICECCS.2013.37"},{"issue":"8","key":"1_CR13","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"100","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 100(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"1_CR14","unstructured":"Butler, R.W., Hagen, G., Maddalon, J.M.: The Chorus conflict and loss of separation resolution algorithms. Technical report, Technical Memorandum NASA\/TM-2013-218030, NASA, Langley Research Center, Hampton VA 23681\u20132199, USA (2013)"},{"issue":"2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10515-007-0008-2","volume":"14","author":"AB Can","year":"2007","unstructured":"Can, A.B., Bultan, T., Lindvall, M., Lux, B., Topp, S.: Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllers. Autom. Softw. Eng. 14(2), 129\u2013178 (2007)","journal-title":"Autom. Softw. Eng."},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: ASE, pp. 702\u2013705. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693137"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/j.scico.2014.06.011","volume":"97","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333\u2013348 (2015)","journal-title":"Sci. Comput. Program."},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 321\u2013330. ACM (2011)","DOI":"10.1145\/1985793.1985838"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/978-3-642-54862-8_54","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C von Essen","year":"2014","unstructured":"von Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 620\u2013635. Springer, Heidelberg (2014)"},{"key":"1_CR21","unstructured":"Gario, M., Micheli, A.: pySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT-Workshop (2015)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Hagen, G., Butler, R., Maddalon, J.: Stratway: a modular approach to strategic conflict resolution. In: Preceedings of 11th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, Virgina Beach, VA (2011)","DOI":"10.2514\/6.2011-6892"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Idris, H.R., Shen, N., Wing, D.J.: Improving separation assurance stability through trajectory flexibility preservation. In: 10th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, p. 9011 (2010)","DOI":"10.2514\/6.2010-9011"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-662-46681-0_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-B Jeannin","year":"2015","unstructured":"Jeannin, J.-B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 21\u201336. Springer, Heidelberg (2015)"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Karr, D.A., Vivona, R.A., Roscoe, D.A., DePascale, S.M., Wing, D.J.: Autonomous operations planner: a flexible platform for research in flight-deck support for airborne self-separation. In: 12th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference and 14th AIAA\/ISSMO Multidisciplinary Analysis and Optimization Conference, p. 5417 (2012)","DOI":"10.2514\/6.2012-5417"},{"key":"1_CR26","unstructured":"Lauderdale, T., Lewis, T., Prevot, T., Ballin, M., Aweiss, A., Guerreiro, N.: Function allocation for separation assurance: research plan, NASA HQ Project Overview, August 2014"},{"key":"1_CR27","unstructured":"Loos, S.M., Renshaw, D., Platzer, A.: Formal verification of distributed aircraft controllers. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, pp. 125\u2013130. ACM, New York (2013). \n                      http:\/\/doi.acm.org\/10.1145\/2461328.2461350"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Mattarei, C., Cimatti, A., Gario, M., Tonetta, S., Kristin Yvonne, R.: Comparing different functional allocations in automated air traffic control design. In: Formal Methods in Computer-Aided Design (FMCAD15) (2015)","DOI":"10.1109\/FMCAD.2015.7542260"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Mehlitz, P.: Trust your model-verifying aerospace system models with Java PathFinder. In: IEEE\/Aero (2008)","DOI":"10.1109\/AERO.2008.4526573"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/11916246_16","volume-title":"Rigorous Development of Complex Fault-Tolerant Systems","author":"C Mu\u00f1oz","year":"2006","unstructured":"Mu\u00f1oz, C., Carre\u00f1o, V.A., Dowek, G.: Formal analysis of the operational concept for the small aircraft transportation system. In: Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.) Rigorous Development of Complex Fault-Tolerant Systems. LNCS, vol. 4157, pp. 306\u2013325. Springer, Heidelberg (2006)"},{"key":"1_CR31","unstructured":"Mu\u00f1oz, C., Siminiceanu, R., Carre\u00f1o, V., Dowek, G.: KB3D Reference Manual-Version 1. NASA (2005)"},{"key":"1_CR32","unstructured":"Vesely, W., Goldberg, F., Roberts, N., Haasl, D.: Fault Tree Handbook. Technical report NUREG-0492, Systems and Reliability Research Office of Nuclear Regulatory Research U.S. (1981)"},{"key":"1_CR33","unstructured":"Wing, D.J., Ballin, M.G., Krishnamurthy, K.: Pilot in command: a feasibility assessment of autonomous flight management operations. In: 24th International Congress of the Aeronautical Sciences (2004)"},{"issue":"3","key":"1_CR34","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/j.scico.2014.04.002","volume":"96","author":"Y Zhao","year":"2014","unstructured":"Zhao, Y., Rozier, K.Y.: Formal specification and verification of a coordination protocol for an automated air traffic control system. Sci. Comput. Program. J. 96(3), 337\u2013353 (2014)","journal-title":"Sci. Comput. Program. J."},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Rozier, K.Y.: Probabilistic model checking for comparative analysis of automated air traffic control systems. In: Proceedings of the 33rd IEEE\/ACM International Conference On Computer-Aided Design (ICCAD 2014), pp. 690\u2013695. IEEE\/ACM, San Jose, November 2014","DOI":"10.1109\/ICCAD.2014.7001427"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41540-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:06:44Z","timestamp":1594685204000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41540-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415390","9783319415406"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41540-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}