Skip to main content

2017 | OriginalPaper | Buchkapitel

5. Software-Verifikation

Beiträge der Münchner Forschung

verfasst von : Dirk Beyer, Rolf Hennicker, Martin Hofmann, Tobias Nipkow, Martin Wirsing

Erschienen in: 50 Jahre Universitäts-Informatik in München

Verlag: Springer Berlin Heidelberg

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

search-config
loading …

Zusammenfassung

Bei der Entwicklung von Software ist es aufgrund ihrer Komplexität erforderlich, automatisierte Verfahren zur Überprüfung der korrekten Funktion einzusetzen. Um die Integration und korrekte Zusammenarbeit verschiedener Komponenten großer Softwaresysteme sicherzustellen, entwickeln Forschergruppen an den Münchner Universitäten sowohl Modell-basierte als auch Quellcode-basierte Techniken. Als Anwendungsbereiche betrachten wir unter anderem Komponenten der Infrastruktur, autonome Systeme und service-orientierte Systeme. Wir setzen Methoden und Algorithmen ein, die den Ingenieur während der Modellierung, der Programmierung und im Releasezyklus mit automatischen Techniken zur Abstraktion, Transformation und Verifikation unterstützen.

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!

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!

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!

Literatur
1.
Zurück zum Zitat F. L. Bauer. Program development by stepwise transformations – The project CIP. Appendix: Programming languages under educational and under professional aspects. In Program Construction, International Summer School, Marktoberdorf, LNCS 69, pages 237–272. Springer, 1978. DOI: 10.1007/BFb0014671 F. L. Bauer. Program development by stepwise transformations – The project CIP. Appendix: Programming languages under educational and under professional aspects. In Program Construction, International Summer School, Marktoberdorf, LNCS 69, pages 237–272. Springer, 1978. DOI: 10.​1007/​BFb0014671
2.
Zurück zum Zitat F. L. Bauer, R. Berghammer, M. Broy, W. Dosch, F. Geiselbrechtinger, R. Gnatz, E. Hangel, W. Hesse, B. Krieg-Brückner, A. Laut, T. Matzner, B. Möller, F. Nickl, H. Partsch, P. Pepper, K. Samelson, M. Wirsing, and H. Wössner. The Munich Project CIP, Volume I: The Wide Spectrum Language CIP-L. LNCS 183. Springer, 1985. DOI: 10.1007/3-540-15187-7 CrossRef F. L. Bauer, R. Berghammer, M. Broy, W. Dosch, F. Geiselbrechtinger, R. Gnatz, E. Hangel, W. Hesse, B. Krieg-Brückner, A. Laut, T. Matzner, B. Möller, F. Nickl, H. Partsch, P. Pepper, K. Samelson, M. Wirsing, and H. Wössner. The Munich Project CIP, Volume I: The Wide Spectrum Language CIP-L. LNCS 183. Springer, 1985. DOI: 10.​1007/​3-540-15187-7 CrossRef
3.
Zurück zum Zitat F. L. Bauer, B. Möller, H. Partsch, and P. Pepper. Formal program construction by transformations – Computer-aided, Intuition-guided Programming. IEEE Trans. Software Eng., 15(2):165–180, 1989. DOI: 10.1109/32.21743 MathSciNetCrossRefMATH F. L. Bauer, B. Möller, H. Partsch, and P. Pepper. Formal program construction by transformations – Computer-aided, Intuition-guided Programming. IEEE Trans. Software Eng., 15(2):165–180, 1989. DOI: 10.​1109/​32.​21743 MathSciNetCrossRefMATH
4.
Zurück zum Zitat S. S. Bauer, P. Mayer, A. Schroeder, and R. Hennicker. On weak modal compatibility, refinement, and the MIO Workbench. In Proc. TACAS, LNCS 6015, pages 175–189. Springer, 2010. S. S. Bauer, P. Mayer, A. Schroeder, and R. Hennicker. On weak modal compatibility, refinement, and the MIO Workbench. In Proc. TACAS, LNCS 6015, pages 175–189. Springer, 2010.
6.
Zurück zum Zitat D. Beyer. Software verification with validation of results (Report on SV-COMP 2017). In Proc. TACAS. Springer, 2017. LNCS 10206, pages 331–349, DOI: 10.1007/978-3-662-54580-5_20 D. Beyer. Software verification with validation of results (Report on SV-COMP 2017). In Proc. TACAS. Springer, 2017. LNCS 10206, pages 331–349, DOI: 10.1007/978-3-662-54580-5_20
7.
Zurück zum Zitat D. Beyer and M. Dangl. Verification-aided debugging: An interactive web-service for exploring error witnesses. In Proc. CAV (2), LNCS 9780, pages 502–509. Springer, 2016. DOI: 10.1007/978-3-319-41540-6_28 D. Beyer and M. Dangl. Verification-aided debugging: An interactive web-service for exploring error witnesses. In Proc. CAV (2), LNCS 9780, pages 502–509. Springer, 2016. DOI: 10.​1007/​978-3-319-41540-6_​28
8.
Zurück zum Zitat D. Beyer, M. Dangl, D. Dietsch, and M. Heizmann. Correctness witnesses: Exchanging verification results between verifiers. In Proc. FSE, pages 326–337. ACM, 2016. DOI: 10.1145/2950290.2950351 D. Beyer, M. Dangl, D. Dietsch, and M. Heizmann. Correctness witnesses: Exchanging verification results between verifiers. In Proc. FSE, pages 326–337. ACM, 2016. DOI: 10.​1145/​2950290.​2950351
9.
Zurück zum Zitat D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, and A. Stahlbauer. Witness validation and stepwise testification across software verifiers. In Proc. FSE, pages 721–733. ACM, 2015. DOI: 10.1145/2786805.2786867 D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, and A. Stahlbauer. Witness validation and stepwise testification across software verifiers. In Proc. FSE, pages 721–733. ACM, 2015. DOI: 10.​1145/​2786805.​2786867
10.
Zurück zum Zitat D. Beyer, S. Gulwani, and D. Schmidt. Combining model checking and data-flow analysis. In E. M. Clarke, T. A. Henzinger, and H. Veith, editors, Handbook on Model Checking. Springer, 2017. D. Beyer, S. Gulwani, and D. Schmidt. Combining model checking and data-flow analysis. In E. M. Clarke, T. A. Henzinger, and H. Veith, editors, Handbook on Model Checking. Springer, 2017.
11.
Zurück zum Zitat D. Beyer, T. A. Henzinger, and G. Théoduloz. Configurable software verification: Concretizing the convergence of model checking and program analysis. In Proc. CAV, LNCS 4590, pages 504–518. Springer, 2007. DOI: 10.1007/978-3-540-73368-3_51 D. Beyer, T. A. Henzinger, and G. Théoduloz. Configurable software verification: Concretizing the convergence of model checking and program analysis. In Proc. CAV, LNCS 4590, pages 504–518. Springer, 2007. DOI: 10.​1007/​978-3-540-73368-3_​51
13.
Zurück zum Zitat D. Beyer and S. Löwe. Explicit-state software model checking based on CEGAR and interpolation. In Proc. FASE, LNCS 7793, pages 146–162. Springer, 2013. DOI: 10.1007/978-3-642-37057-1_11 D. Beyer and S. Löwe. Explicit-state software model checking based on CEGAR and interpolation. In Proc. FASE, LNCS 7793, pages 146–162. Springer, 2013. DOI: 10.​1007/​978-3-642-37057-1_​11
14.
Zurück zum Zitat D. Beyer, S. Löwe, E. Novikov, A. Stahlbauer, and P. Wendler. Precision reuse for efficient regression verification. In Proc. ESEC/FSE, pages 389–399. ACM, 2013. DOI: 10.1145/2491411.2491429 D. Beyer, S. Löwe, E. Novikov, A. Stahlbauer, and P. Wendler. Precision reuse for efficient regression verification. In Proc. ESEC/FSE, pages 389–399. ACM, 2013. DOI: 10.​1145/​2491411.​2491429
16.
Zurück zum Zitat A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. CONCUR, LNCS 1243, pages 135–150. Springer, 1997. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. CONCUR, LNCS 1243, pages 135–150. Springer, 1997.
17.
Zurück zum Zitat M. Broy. Towards a formal foundation of the specification and description language SDL. Formal Aspects of Computing, 3(1):21–57, 1991.CrossRefMATH M. Broy. Towards a formal foundation of the specification and description language SDL. Formal Aspects of Computing, 3(1):21–57, 1991.CrossRefMATH
18.
Zurück zum Zitat M. Broy and G. Ştefănescu. The algebra of stream processing functions. Theoretical Computer Science, 258(1):99–129, 2001.MathSciNetCrossRefMATH M. Broy and G. Ştefănescu. The algebra of stream processing functions. Theoretical Computer Science, 258(1):99–129, 2001.MathSciNetCrossRefMATH
19.
Zurück zum Zitat E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. Logic of Programs 1981, LNCS 131, pages 52–71. Springer, 1982. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. Logic of Programs 1981, LNCS 131, pages 52–71. Springer, 1982.
20.
Zurück zum Zitat E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752–794, 2003.MathSciNetCrossRefMATH E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752–794, 2003.MathSciNetCrossRefMATH
21.
22.
Zurück zum Zitat J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded programs. ACM Trans. Program. Lang. Syst., 36(3):9, 2014.CrossRef J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded programs. ACM Trans. Program. Lang. Syst., 36(3):9, 2014.CrossRef
23.
Zurück zum Zitat J. Esparza, M. Hofmann, T. Nipkow, H. Seidl, DFG Graduiertenkolleg GRK 1480: Programm und Modellanalyse (PUMA), 2008-2017, 2007. J. Esparza, M. Hofmann, T. Nipkow, H. Seidl, DFG Graduiertenkolleg GRK 1480: Programm und Modellanalyse (PUMA), 2008-2017, 2007.
24.
Zurück zum Zitat R. Grabowski, M. Hofmann, and K. Li. Type-based enforcement of secure programming guidelines – Code injection prevention at SAP. In Proc. FAST, LNCS 7140, pages 182–197. Springer, 2011. DOI: 10.1007/978-3-642-29420-4_12 R. Grabowski, M. Hofmann, and K. Li. Type-based enforcement of secure programming guidelines – Code injection prevention at SAP. In Proc. FAST, LNCS 7140, pages 182–197. Springer, 2011. DOI: 10.​1007/​978-3-642-29420-4_​12
25.
Zurück zum Zitat T. C. Hales, J. Harrison, S. McLaughlin, T. Nipkow, S. Obua, and R. Zumkeller. A revision of the proof of the Kepler conjecture. Discrete and Computational Geometry, 44:1–34, 2010.MathSciNetCrossRefMATH T. C. Hales, J. Harrison, S. McLaughlin, T. Nipkow, S. Obua, and R. Zumkeller. A revision of the proof of the Kepler conjecture. Discrete and Computational Geometry, 44:1–34, 2010.MathSciNetCrossRefMATH
26.
Zurück zum Zitat R. Hennicker, M. Bidoit, and T.-S. Dang. On synchronous and asynchronous compatibility of communicating components. In Proc. COORDINATION, LNCS 9686, pages 138–156. Springer, 2016. R. Hennicker, M. Bidoit, and T.-S. Dang. On synchronous and asynchronous compatibility of communicating components. In Proc. COORDINATION, LNCS 9686, pages 138–156. Springer, 2016.
27.
Zurück zum Zitat R. Hennicker, S. Janisch, A. Kraus, and M. Ludwig. A web-based modelling and decision support system to investigate global change and the hydrological cycle in the Upper Danube basin. In Regional Assessment of Global Change Impacts – The Project GLOWA-Danube, chapter 2, pages 19–28. Springer, 2016.CrossRef R. Hennicker, S. Janisch, A. Kraus, and M. Ludwig. A web-based modelling and decision support system to investigate global change and the hydrological cycle in the Upper Danube basin. In Regional Assessment of Global Change Impacts – The Project GLOWA-Danube, chapter 2, pages 19–28. Springer, 2016.CrossRef
28.
Zurück zum Zitat R. Hennicker, A. Klarl, and M. Wirsing. Model-checking Helena ensembles with Spin. In Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, LNCS 9200, pages 331–360. Springer, 2015. R. Hennicker, A. Klarl, and M. Wirsing. Model-checking Helena ensembles with Spin. In Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, LNCS 9200, pages 331–360. Springer, 2015.
29.
Zurück zum Zitat M. M. Hölzl, N. Koch, M. Puviani, M. Wirsing, and F. Zambonelli. The ensemble development life cycle and best practices for collective autonomic systems. In Software Engineering for Collective Autonomic Systems – The ASCENS Approach, LNCS 8998, pages 325–354. Springer, 2015. DOI: 10.1007/978-3-319-16310-9_9 M. M. Hölzl, N. Koch, M. Puviani, M. Wirsing, and F. Zambonelli. The ensemble development life cycle and best practices for collective autonomic systems. In Software Engineering for Collective Autonomic Systems – The ASCENS Approach, LNCS 8998, pages 325–354. Springer, 2015. DOI: 10.​1007/​978-3-319-16310-9_​9
31.
Zurück zum Zitat G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood. Verified Java-Bytecode Verification. PhD thesis, Institut für Informatik, Technische Universität München, 2003. G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood. Verified Java-Bytecode Verification. PhD thesis, Institut für Informatik, Technische Universität München, 2003.
32.
Zurück zum Zitat G. Klein et al. seL4: Formal verification of an operating-system kernel. Commun. ACM, 53(6):107–115, 2010.CrossRef G. Klein et al. seL4: Formal verification of an operating-system kernel. Commun. ACM, 53(6):107–115, 2010.CrossRef
34.
35.
Zurück zum Zitat M. Wirsing, A. Clark, S. Gilmore, M. Hölzl, A. Knapp, N. Koch, and A. Schroeder. Semantic-based development of service-oriented systems. In Proc. FORTE, LNCS 4229, pages 24–45. Springer, 2006. M. Wirsing, A. Clark, S. Gilmore, M. Hölzl, A. Knapp, N. Koch, and A. Schroeder. Semantic-based development of service-oriented systems. In Proc. FORTE, LNCS 4229, pages 24–45. Springer, 2006.
36.
Zurück zum Zitat M. Wirsing and M. M. Hölzl, editors. Rigorous Software Engineering for Service-Oriented Systems – Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing. LNCS 6582. Springer, 2011. DOI: 10.1007/978-3-642-20401-2 M. Wirsing and M. M. Hölzl, editors. Rigorous Software Engineering for Service-Oriented Systems – Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing. LNCS 6582. Springer, 2011. DOI: 10.​1007/​978-3-642-20401-2
37.
Zurück zum Zitat M. Wirsing, M. M. Hölzl, N. Koch, and P. Mayer, editors. Software Engineering for Collective Autonomic Systems – The ASCENS Approach. LNCS 8998. Springer, 2015. DOI: 10.1007/978-3-319-16310-9 M. Wirsing, M. M. Hölzl, N. Koch, and P. Mayer, editors. Software Engineering for Collective Autonomic Systems – The ASCENS Approach. LNCS 8998. Springer, 2015. DOI: 10.​1007/​978-3-319-16310-9
Metadaten
Titel
Software-Verifikation
verfasst von
Dirk Beyer
Rolf Hennicker
Martin Hofmann
Tobias Nipkow
Martin Wirsing
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-54712-0_5