Wir entwickeln Verfahren für die Verifikation von eingebetteten Steuerungssystemen, mit einer Spezialisierung auf automatisiertes und autonomes Fahren. Die Gewährleistung der Sicherheit und Korrektheit dieser cyber-physikalischen Systeme ist angesichts ihrer zunehmenden Autonomie, Komplexität und der Vielzahl betrieblicher Bedingungen von entscheidender Bedeutung. Eine zentrale Herausforderungen dabei ist die eingesetzte komplexe Software, oft einschließlich neuronaler Netzwerkkomponenten, gegen Sicherheits- und Funktionsspezifikationen zu validieren. Unsere Forschung entwickelt skalierbare und automatisierte Verifizierungs-Frameworks, die formale Methoden mit praktischer Implementierung verbinden.
Verifikation vonSoftware
Wir entwickeln skalierbare Verifikationslösungen auf Code-Ebene, die eingebettete Steuerimplementierungen direkt gegen Sicherheitsvorgaben überprüfen. Dies umfasst sowohl traditionelle adaptive Geschwindigkeitsregelung (adaptive cruise control) Software als auch auf neuronalen Netzwerken basierende Regler. Durch die Kombination von bounded model checking mit kompositionellen Annahme-Garantie-Anforderungen überprüfen wir effizient Sicherheitsmerkmale im geschlossenen Regelkreis. Das CoCoSaFe-Framework veranschaulicht diesen Ansatz und überprüft innerhalb von Minuten mehrere Regler, die im industriellen Context verwendet werden.
Model Checking von Entscheidungsfindungskomponenten
Wir nutzen automatisierte Verhaltensabstraktion und Model Checking, um sowohl traditionelle Regler als auch Komponenten mit künstlicher Intelligenz zu analysieren. Für neuronale Netzwerk-basierte Regler für die prädiktive Regelung verwenden wir Invarianzmengen kombiniert mit neuronalen Netzwerkverifizierungstools, um die Sicherheit zu zertifizieren oder Gegenbeispiele zu finden. Dieser hybride Ansatz bietet Garantien, selbst für erlernte Regler, die in unsicheren Umgebungen arbeiten.
Überprüfen der Softwareportabilität für verschiedene Hardware
Um einen sicheren Einsatz über verschiedene Hardwarekonfigurationen hinweg zu gewährleisten, haben wir ein automatisches Portabilitätsverifikationsframework entwickelt. Dafür werden formale Modelle für die konfigurationstypische Fahrzeugdynamik, Wahrnehmung und Aktion erstellt und dafür Invarianzmengen innerhalb jedes Betriebsdesignbereichs berechnet. Die Software für automatisiertes Fahren wird dann dynamisch über jede Invarianzmenge eines Zielhardware-Setups überprüft, um eine schnelle Integration, Tests und Software-Updates mit funktionalen Sicherheitsgarantien zu ermöglichen.
Laufzeitüberwachung und -verifikation
Wir entwerfen leichtgewichtige Laufzeitmonitore für die autonome Roboternavigation und eingebettete Systeme. Diese Monitore nutzen offline berechnete Sicherheitszertifikate und Fortschritts-/Fehlerkriterien, um Sicherheitsverletzungen vorausschauend und mit niedrigen Fehlalarmraten zu erkennen. Der Ansatz benötigt lediglich gefilterte Zustandsschätzungen, was eine effiziente Laufzeitverifikation von Black-Box-Systemen in dynamischen, unsicheren Umgebungen ermöglicht und die Betriebssicherheit ohne umfangreiche Berechnungen an Bord verbessert.
Lernbasierte Falsifikation
Wir haben ein lernbasiertes Falsifikations-Framework entwickelt, das adversarielle verstärkungslernende Agenten mit modellbasierten Falsifikatoren kombiniert, um effizient herausfordernde Szenarien zu generieren, die Sicherheitsvorgaben verletzen. Diese hybride Methode beschleunigt die Falsifikation in Simulationen und deckt nicht-triviale Sicherheitsverletzungen für Regler, wie z.B. die adaptive Geschwindigkeitsregelung (adaptive cruise control) auf, wodurch reine lern- oder modellbasierte Falsifikationsmethoden übertroffen werden.
Beteiligte:
Prof. Dr.-Ing. Vladislav Nenchev
Dipl.-Ing. Prodromos Sotiriadis
Kooperationspartner:
University of York, UK
University of Padova, IT
BMW