Ein Werkzeugkasten für die Erreichbarkeitsanalyse hybrider Systeme mittels geometrischer Approximationen

• Antragstellerinnen / Antragsteller: Professor Dr.-Ing. Stefan Kowalewski; Professorin Dr. Erika Ábrahám
• Fachliche Zuordnung: Theoretische Informatik ; Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2013 bis 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 227484301

Hybride Systeme sind Systeme mit gemischtem diskret-kontinuierlichem Verhalten. Typische Beispiele sind physikalische Systeme, welche von digitalen Kontrollern gesteuert werden. Da solche Systeme oft sicherheitskritisch sind, wurde in der Vergangenheit viel in die Entwicklung von Algorithmen und Werkzeugen für die Analyse dieser Systeme investiert. Auch wenn in dem letzten Jahrzehnt viele große Errungenschaften in diesem Bereich hervorgegangen sind, ist die Anwendbarkeit aktueller Techniken immer noch eingeschränkt und bedarf weiterer Verbesserungen.In der ersten Phase unseres HyPro Projektes haben wir eine Software-Bibliothek, welche die Implementierung neuer Algorithmen für die Erreichbarkeitsanalyse hybrider Systeme erleichtern soll, entwickelt. Des Weiteren haben wir unser Tool Flow* entwickelt, welches bereits rege Verwendung findet, da es hybride Systeme deren Dynamik durch nicht-lineare Differentialgleichungen beschrieben ist analysieren kann. Zusätzlich haben wir eine Benchmark-Bibliothek erstellt und mit deren Hilfe vorhandene Tools für die Erreichbarkeitsanalyse hybrider Systeme ausführlich getestet und miteinander verglichen. Während der ersten Projektphase haben wir mehrere Probleme, welche die erfolgreiche Analyse hybrider Systeme mit aktueller Software erschweren, identifiziert. In diesem Antrag stellen wir Forschungsinhalte für eine Verlängerung unseres HyPro Projektes vor, um mithilfe unserer HyPro Bibliothek Lösungen für einige dieser herausfordernden Probleme zu finden. Während die meisten Technologien statische Suchheuristiken verwenden, stellen wir uns das Ziel, dynamische Suchstrategien zu entwickeln, welche die kontext-sensitive Anpassung der Suchparameter erlauben. Neben der Entwicklung eines generellen Ansatzes wollen wir spezialisierte Strategien für die Gegenbeispielerzeugung, für die Analyse von Modellen mit Zeno-Verhalten und für die Analyse von probabilistischen hybriden Systemen entwickeln. Um die Effizienz weiter steigern zu können, werden wir uns außerdem mit Themen aus den Bereichen der Parallelisierung und der kompositionellen Analyse befassen.

• DFG-Verfahren: Sachbeihilfen