Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

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

verfasst von : Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, Kristin Yvonne Rozier

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Nächstes Kapitel Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers
Literatur
1.
2.
3.
4.
5.
6.
Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993)CrossRef
7.
ARP4754A guidelines for development of civil aircraft and systems. In: SAE, December 2010
8.
ARP4761 guidelines and methods for conducting the safety assessment process on civil airborne systems and equipment. In: SAE, December 1996
9.
Bauer, C., Lagadec, K., Bès, C., Mongeau, M.: Flight control system architecture optimization for fly-by-wire airliners. J. Guidance Control Dyn. 30(4), 1023–1029 (2007)CrossRef
10.
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–539. Springer, Heidelberg (2016)CrossRef
11.
Bozzano, M., Cimatti, A., Griggio, A., Mattarei, C.: Efficient anytime techniques for model-based safety analysis. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 603–621. Springer, Heidelberg (2015)CrossRef
12.
Bozzano, M., Cimatti, A., Mattarei, C.: Automated analysis of reliability architectures. In: 18th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 198–207. IEEE, July 2013
13.
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 100(8), 677–691 (1986)CrossRefMATH
14.
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–2199, USA (2013)
15.
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–178 (2007)CrossRef
16.
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–342. Springer, Heidelberg (2014)
17.
Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: ASE, pp. 702–705. IEEE (2013)
18.
Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333–348 (2015)CrossRef
19.
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–330. ACM (2011)
20.
von Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 620–635. Springer, Heidelberg (2014)CrossRef
21.
Gario, M., Micheli, A.: pySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT-Workshop (2015)
22.
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)
23.
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)
24.
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–36. Springer, Heidelberg (2015)
25.
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)
26.
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
27.
28.
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)
29.
Mehlitz, P.: Trust your model-verifying aerospace system models with Java PathFinder. In: IEEE/Aero (2008)
30.
Muñoz, C., Carreño, 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–325. Springer, Heidelberg (2006)CrossRef
31.
Muñoz, C., Siminiceanu, R., Carreño, V., Dowek, G.: KB3D Reference Manual-Version 1. NASA (2005)
32.
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)
33.
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)
34.
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–353 (2014)CrossRef
35.
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–695. IEEE/ACM, San Jose, November 2014
Metadaten
Titel
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration
verfasst von
Marco Gario
Alessandro Cimatti
Cristian Mattarei
Stefano Tonetta
Kristin Yvonne Rozier
Copyright-Jahr
2016
Buch
Computer Aided Verification

Print ISBN: 978-3-319-41539-0

Electronic ISBN: 978-3-319-41540-6

Copyright-Jahr: 2016

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

Premium Partner

    Bildnachweise