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

• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2004 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5485999

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