Detailseite
Projekt
TRR 14: AVACS - Automatische Verifikation und Analyse komplexer Systeme
Fachliche Zuordnung
Informatik, System- und Elektrotechnik
Förderung
Förderung von 2004 bis 2015
Projektkennung
Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5485999
In diesem Projekt werden Methoden und Verfahren zur mathematischen Analyse von Modellen von komplexen sicherheitskritischen eingebetteten Systemen entwickelt. Solche Systeme sind beispielsweise Flugzeuge, Züge, Autos oder andere Artefakte, deren Versagen Leben gefährden kann.
Ziel ist, den heutigen Stand der Technik dieser Methoden, mit dem nur jeweils einzelne Aspekte solcher Systeme behandelbar sind (wie z.B. Nebenläufigkeit, Zeitverhalten, kontinuierliche Kontrolle, Stabilität, Mobilität, Datenstrukturen, Hardwarebeschränkungen, Modularität, Verfeinerungsebenen), derart zu verbessern, dass eine umfassende, ganzheitliche Verifikation dieser Systeme möglich wird.
Durch Verbesserung und erhöhte Automatisierung von Basis-Verifikations-Techniken (wie z.B. abstrakte Interpretation, lineare Programmierung, Constraint Solving, Lyapunov Funktionen, automatische Entscheidungsprozeduren, automatenbasierte Verifikation, heuristische Suche) und durch eine tief gehende, zielgerichtete Integration dieser Techniken sollen insbesondere solche Modelle durch automatische Verifikations- und Analysemethoden behandelbar werden, deren Komplexität diese Behandlung heute noch ausschließt. Mit Komplexität ist hier sowohl Systemgröße gemeint als auch logische Komplexität induziert durch Interferenzen zwischen den verschiedenen Teilaspekten. Durch Ausnutzung von Entwurfs- und Designparadigmen (mathematisch dargestellt als Zerlegungs-Sätze, die komplexe Systeme in kleinere, behandelbare Teilsysteme bzw. -aspekte aufteilen) wird die Kombination der einzelnen, komplementären Verifikationstechniken Synergien erzeugen, die in heutigen Verifikationswerkzeugen nicht gefunden werden können.
Ziel ist, den heutigen Stand der Technik dieser Methoden, mit dem nur jeweils einzelne Aspekte solcher Systeme behandelbar sind (wie z.B. Nebenläufigkeit, Zeitverhalten, kontinuierliche Kontrolle, Stabilität, Mobilität, Datenstrukturen, Hardwarebeschränkungen, Modularität, Verfeinerungsebenen), derart zu verbessern, dass eine umfassende, ganzheitliche Verifikation dieser Systeme möglich wird.
Durch Verbesserung und erhöhte Automatisierung von Basis-Verifikations-Techniken (wie z.B. abstrakte Interpretation, lineare Programmierung, Constraint Solving, Lyapunov Funktionen, automatische Entscheidungsprozeduren, automatenbasierte Verifikation, heuristische Suche) und durch eine tief gehende, zielgerichtete Integration dieser Techniken sollen insbesondere solche Modelle durch automatische Verifikations- und Analysemethoden behandelbar werden, deren Komplexität diese Behandlung heute noch ausschließt. Mit Komplexität ist hier sowohl Systemgröße gemeint als auch logische Komplexität induziert durch Interferenzen zwischen den verschiedenen Teilaspekten. Durch Ausnutzung von Entwurfs- und Designparadigmen (mathematisch dargestellt als Zerlegungs-Sätze, die komplexe Systeme in kleinere, behandelbare Teilsysteme bzw. -aspekte aufteilen) wird die Kombination der einzelnen, komplementären Verifikationstechniken Synergien erzeugen, die in heutigen Verifikationswerkzeugen nicht gefunden werden können.
DFG-Verfahren
Transregios
Internationaler Bezug
Tschechische Republik
Abgeschlossene Projekte
- H01 - Deduction and Automata Based Approaches (Teilprojektleiter Ganzinger, Harald )
- H02 - Bounded Model Checking and Inductive Verification of Hybrid Systems (Teilprojektleiter Becker, Bernd )
- H02 - Constraint-basierte Verfikation hybrider Systeme (Teilprojektleiter Althaus, Ernst ; Becker, Bernd ; Fränzle, Martin ; Weidenbach, Christoph )
- H03 - Automatisierte Verifikation kooperierender Verkehrssysteme (Teilprojektleiterinnen / Teilprojektleiter Althaus, Ernst ; Damm, Werner ; Olderog, Ernst-Rüdiger ; Scholl, Christoph ; Sofronie-Stokkermans, Viorica ; Waldmann, Uwe )
- H04 - Automatische Stabilitätsbeweisführung für Hybride Systeme (Teilprojektleiterinnen / Teilprojektleiter Fränzle, Martin ; Hermanns, Holger ; Podelski, Andreas ; Theel, Oliver ; Wolf, Verena )
- R01 - Über Realzeitautomaten hinaus (Teilprojektleiterinnen / Teilprojektleiter Finkbeiner, Bernd ; Fränzle, Martin ; Olderog, Ernst-Rüdiger ; Podelski, Andreas ; Sofronie-Stokkermans, Viorica )
- R02 - Zeitanalyse, Scheduling und Verteilung von Echtzeittasks (Teilprojektleiter Althaus, Ernst ; Damm, Werner ; Hack, Sebastian ; Reineke, Jan ; Wilhelm, Reinhard )
- R03 - Heuristisches Suchen und abstraktes Modell-Checking für Realzeit-Systeme (Teilprojektleiter Finkbeiner, Bernd ; Nebel, Bernhard ; Podelski, Andreas )
- S01 - Kompositionelle Verifikation komplexer Systeme (Teilprojektleiter Becker, Bernd ; Finkbeiner, Bernd ; Nebel, Bernhard ; Scholl, Christoph )
- S02 - Dynamische Kommunikationssysteme (Teilprojektleiter Damm, Werner ; Finkbeiner, Bernd ; Hermanns, Holger ; Podelski, Andreas ; Weidenbach, Christoph )
- S03 - Verifikation von Verlässlichkeitseigenschaften (Teilprojektleiterinnen / Teilprojektleiter Becker, Bernd ; Hermanns, Holger ; Theel, Oliver ; Wolf, Verena )
- T01 - Exakte Nichterreichbarkeitsanalyse für eingebetteten C Code durch arithmetisches Constraint Solving (Teilprojektleiter Becker, Bernd ; Fränzle, Martin )
- Z01 - Zentrale Aufgaben des SFB/Transregio (Teilprojektleiter Becker, Bernd ; Damm, Werner ; Finkbeiner, Bernd )
Antragstellende Institution
Carl von Ossietzky Universität Oldenburg
Mitantragstellende Institution
Albert-Ludwigs-Universität Freiburg; Universität des Saarlandes
Beteiligte Institution
Max-Planck-Institut für Informatik
Sprecher
Professor Dr. Werner Damm
