Automatische Stabilitätsbeweisführung für Hybride Systeme (H04)

Das Ziel des Teilprojektes ist die Bereitstellung der prototypischen Implementierung eines Werkzeugszum automatischen Nachweis der Konvergenz sowie der Stabilität hybrider Systeme. Als Eingabeerwartet das Werkzeug die Spezifikation eines hybriden Systems und eine entsprechend detaillierteBeschreibung der Beweisverpflichtung. Die Beweisverpflichtung kann eine von mehreren möglichenArten von Stabilität umfassen. Zudem kann sie  neben anderen Angaben  aus Verpflichtungen bestehen,wie beweise, dass ausgehend von einem Zustand, in dem P gilt, ein Zustand in dem P gilt, inweniger als t Zeiteinheiten erreicht werden kann. Sollte das Werkzeug nicht in der Lage sein, Konvergenzbzw. Stabilität wie gefordert automatisch nachzuweisen, dann wird stattdessen Informationzurückgeliefert, anhand der ein Re-Design des Reglers durchgeführt werden kann, derart, dass diesesdas resultierende hybride System konvergent macht bzw. stabilisiert.

DFG-Verfahren Transregios

Teilprojekt zu TRR 14:  AVACS - Automatische Verifikation und Analyse komplexer Systeme

Antragstellende Institution Carl von Ossietzky Universität Oldenburg

Mitantragstellende Institution Albert-Ludwigs-Universität Freiburg; Universität des Saarlandes

Teilprojektleiterinnen / Teilprojektleiter Professor Dr. Martin Fränzle; Professor Dr.-Ing. Holger Hermanns; Professor Dr. Andreas Podelski; Professor Dr.-Ing. Oliver Theel; Professorin Dr. Verena Wolf