Im Sonderforschungsbereich/Transregio AVACS werden Methoden und Verfahren zur mathematischen Verifikation und Analyse von Modellen komplexer sicherheitskritischer eingebetteter Systeme entwickelt. Solche Systeme, deren Versagen Leben gefährden kann, sind beispielsweise Flugzeuge, Züge, Autos oder auch Verbünde solcher Fahr-zeuge. Ziel ist, den heutigen Stand der Technik für Verifikations- und Analyse-Methoden, mit dem nur jeweils einzelne Aspekte dieser Systeme behandelbar sind, derart zu ver-bessern, dass eine umfassende, ganzheitliche Verifikation dieser Systeme möglich wird.

• AVACS untersucht mathematische Modelle und deren Beziehungen, wie sie in den verschiedenen Designebenen beim Entwurf sicherheitskritischer eingebetteter Systeme auftreten. Solche Modelle reichen von klassischen nicht-deterministischen Transitionssystemen bis hin zu probabilistischen, zeitbehafteten und hybriden Modellen, sowie zu Modellen, die die dynamische Kommunikationsstruktur solcher Systeme beschreiben.

• Die untersuchten Modellklassen decken alle typischen Systemstrukturen dieser Anwendungsdomäne ab und beschreiben, wie komplexe Systeme hierarchisch aufgebaut werden können. Sie beinhalten Modelle verteilter Zielarchitekturen (wie z.B. durch hierarchische Bussysteme verbundene Steuergeräte), Task-Modelle (z.B. hierarchische Tasksysteme mit Kommunikations- und Zeitanforderungen), Spezifikationsmodelle von Steuergeräten, Systemmodelle (z.B. Fahrzeuge) und Modelle von Systemen, deren Kompenenten selbst vollständige Systeme sind (z.B. zur Koordination von Manövern mehrerer Fahrzeuge).

• Die untersuchten Modelle der Zeit sind dabei ausdrucksstark genug, um Zeitverhalten in allen Ebenen des Entwurfsraums solcher Applikationen zu beschreiben. Dies beinhaltet z.B. physikalische Latenzen von Fahrzeugen bei koordinierten Manövern, Zeitanforderungen auf Systemebene (z.B. Anforderungen an Reaktionszeiten auf externe Ereignisse oder für Kommunikationsprotokolle), dense-time Modelle von geschlossenen Regelkreisen, Modelle von Steuersystemen mit diskreter Zeit, end-to-end deadlines von Task-Ketten und Worst-Case-Execution Times für die Ausführung von Tasks auf modernen Prozessoren.

• AVACS entwickelt weitgehend automatische Techniken zur Verifikation oder Falsi-fikation von Modellen aus diesem reichhaltigen Modellraum gegenüber Klassen von in geeigneten Logiken formalisierten Anforderungen bzgl. Zeitverhalten, Sicherheit (Safety), probabilistische Erreichbarkeit, Stabilität und weiteren Eigenschaften.

• Die von AVACS entwickelten Methoden und Techniken zielen dabei auch auf die Erstellung von formalen Beweisen für komplette Systeme aus garantierten Eigenschaften der Komponenten eines solchen Systems. So sollen z.B. Anforderungen an das Gesamtsystem (wie z.B. die Vermeidung von Kollisionen bei der Durchführung koordinierter Fahrzeugmanöver) abgestützt werden auf Worst-Case-Execution-Times der Tasks, die die Steuerfunktionen für solche Manöver implementieren.