Number of cases campus Koblenz: 1 (warning level Gelb until 02.12.2020) Action plan

Automatisierte Verifikation kooperierender Verkehrssysteme (TRR 14: AVACS - Automatische Verifikation und Analyse komplexer Systeme)

(AVACS-H3)

Period: Jan 01, 2004 - Dec 31, 2015
Status: abgeschlossen

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.


Project partner

Prof. Dr. Viorica Sofronie-Stokkermans, Max-Planck-Institut für Informatik und Universität Koblenz-Landau
Dr. Uwe Waldmann, Max-Planck-Institut für Informatik
Prof. Dr. Christoph Scholl, Albert-Ludwigs-Universität Freiburg

Prof. Dr. Ernst Althaus, Johannes Gutenberg-Universität Mainz und Max-Planck-Institut für Informatik
Prof. Dr. Ernst-Rüdiger Olderog, Carl von Ossietzky Universität Oldenburg
Prof. Dr. Werner Damm, Carl von Ossietzky Universität Oldenburg