Kurzfassung

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,...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.» weiterlesen» einklappen