Stefan Schupp: State Set Representations for Hybrid Systems Reachability Analysis

 

Immer häufiger werden digitale Controller zur Steuerung von kontinuierlichen, zum Beispiel physikalischen, Prozessen eingesetzt, sodass auch der Bedarf an Verifikation dieser so genannten hybriden Systeme gestiegen ist.

In meiner Arbeit konzentriere ich mich auf flowpipe-Konstruktion als eine der Methoden, hybride Systeme durch Erreichbarkeitsanalyse zu verifizieren. Dabei wird versucht, die Menge der erreichbaren Zustände eines gegebenen Systems durch eine Menge von geometrischen Objekten zu überapproximieren, zum Beispiel Boxen, konvexe Polyeder, Support Functions oder Zonotope. Ich habe dazu die am häufigsten eingesetzten Zustandsraumdarstellungen gesammelt und in der frei verfügbaren C++ Bibliothek HyPro implementiert. Um Modularität unabhängig von der verwendeten Darstellung zu garantieren, nutzen alle implementierten Darstellungen ein einheitliches Interface. Des Weiteren stellen wir Konvertierungs- und Reduktionsmethoden zur Verfügung. Die Bibliothek enthält außerdem Datenstrukturen und Zusatzfunktionen, zum Beispiel zum Einlesen oder Ausgeben von Systemen/Zustandsraum-Mengen, welche benötigt werden, um einen Flowpipe-Konstruktion-basierten Erreichbarkeitsalgorithmus zu implementieren.

Um die allgemeine Anwendbarkeit dieser Bibliothek zu zeigen, implementiere ich zur Zeit das Erreichbarkeitsanalyse-Programm HyDRA, das noch nicht veröffentlicht ist, welches die klassische Flowpipe-Konstruktion um einige neue Ansätze erweitert. Dies beinhaltet die Wahl der Zustandsraumdarstellung abhängig von der Dynamik des Systems, Pfadverfeinerung, um unechte Gegenbeispiele zu falsifizieren und vor Kurzem auch die Parallelisierung des Ansatzes.