ELITE NETZWERK BAYERN

Deutsch  Language Icon  |  Gebärdensprache  |  Leichte Sprache  |  Kontakt


Forschungsarbeit

Algebraische Kalküle für hybride Systeme

Von Peter Höfner (20.04.2010)

Fehlerhafte Software hat in den letzten Jahrzehnten zahlreiche Menschenleben gefordert, Umweltschäden hervorgerufen und regelmäßig zu enormen wirtschaftlichen Verlusten geführt. Besonders fehleranfällig sind hierbei Systeme, welche ständig mit ihrer Umwelt interagieren, da sie auf diese flexibel, aber dennoch vorhersagbar reagieren müssen. Anders als für reine Softwaresysteme wie Büroanwendungen, sind Korrektheitsanforderungen in diesen Bereichen besonders hoch – ein Airbag, der sich zu spät öffnet, ist nicht akzeptabel.

Solche sicherheitskritische Systeme können meistens als so genannte hybride Systeme charakterisiert werden. Bei diesen Systemen besteht ein Wechselspiel zwischen kontinuierlichem Systemverhalten und Kontrollereignissen zu diskreten Zeitpunkten, die Zustandswechsel auslösen. Anwendungsgebiete reichen von Steuerungselementen über Medizintechnik bis hin zu Avionik. Aber auch chemische und biologische Systeme können mittels solcher Systeme mathematisch exakt beschrieben werden.

Ein beschrankter Bahnübergang als Beispiel eines hybriden Systems[Bildunterschrift / Subline]: Ein beschrankter Bahnübergang als Beispiel eines hybriden Systems; rechts oben: klassische Modellierung mittels Graphen; unten: neue algebraische Charakterisierung.

Hybride Systeme sind jedoch häufig so komplex, dass eine computergestützte Verifikation auch mit den heute verfügbaren großen Speicher- und Rechenkapazitäten nicht durchführbar ist. Ziel der Doktorarbeit ist es Untersuchungen zu einer kompakteren Behandlungsmöglichkeit von Verifikationsaufgaben anzustellen. Zentrales Interesse finden hierbei algebraische Techniken, in denen Systeme durch Gleichungsregeln – ähnlich den aus der Schulalgebra bekannten – beschrieben werden. Die generellen Vorteile eines algebraischen Ansatzes sind vor allem Klarheit und Einfachheit, insbesondere im Hinblick auf (computerunterstützbare) Rechenregeln. Die entwickelte algebraische Charakterisierung hybrider Systeme  ermöglicht es beispielsweise, Sicherheitsaspekte mittels einfacher algebraischer Umformungen zu überprüfen. Ferner bietet dieser Ansatz den Vorteil, dass Standard-Computer-Algebrasysteme verwendet werden können. So können Theorembeweiser eingesetzt werden, um fundamentale Eigenschaften hybrider Systeme automatisch zu verifizieren.

Im letzten Jahrzehnt wurden Dutzende unterschiedlicher Logiken für hybride Systeme eingesetzt: Angefangen von klassischer Aussagenlogik über modale und temporale Logiken bis hin zu eigens für diese Systeme entwickelten Logiken. Die meisten dieser Logiken sind für sich wohlverstanden. Aber auf Grund der Vielzahl von verwendeten Begriffe sowie ihrer unterschiedlichen Notation und Bedeutung ist eine uniforme Behandlung der Logiken und ihrer Beziehungen zueinander sehr schwierig. In der Doktorarbeit werden daher Untersuchungen zu einer kompakteren und einheitlichen Behandlung angestellt. Zentrales Interesse finden hierbei dieselben algebraischen Techniken wie zur Beschreibung von hybriden Systemen. Durch Algebraisierung ist es möglich, Beziehungen zwischen Logiken aufzuzeigen und, für die Doktorarbeit von besonderer Bedeutung, diese Logiken in einer einheitlichen und systematischen Weise auf hybride Systeme anzuwenden.

Die Forschungsergebnisse umfassen grundlegende Methoden zur Analyse hybrider Systeme und münden in eine kohärente Familie algebraischer Kalküle für hybride Systeme. Die Anwendbarkeit und Relevanz der Theorie ist durch erste Fallstudien belegt.


Dr. Peter Höfner
Peter Höfner
* 1978

Stationen
  • Juli 2009
  • Doktor der Naturwissenschaften (Dr. rer-nat)
  • seit Juli 2007
  • Wissenschaftler an der Universität Augsburg
  • Aug. 2006 - Juni 2007
  • Gastwissenschaftler an der Universität Sheffield (Vereinigtes Königreich)
  • Dez. 2003 - Juli 2006
  • Wissenschaftler an der Universität Augsburg
  • Okt. 1998 - Okt. 2003
  • Studium der Mathematik an der Universität Augsburg, Abschluss als Diplom-Mathematiker

Aktuelle Veröffentlichungen
  • *P. Höfner, B. Möller: "An Algebra of Hybrid Systems". In. Journal of Logic and Algebraic Programming 78, pp. 74-97, 2009.
  • *P. Höfner, B. Möller: "Algebraic Neighbourhood Logic". In: Journal of Logic and Algebraic Programming 76 (Special Issue), pp.35-59, 2008.
  • *P. Höfner, R. Khedri, B. Möller: "Algebraic View Reconciliation". In: A. Cerone and S. Gruner (eds.): Software Engineering and Formal Methods (SEFM '08) pp. 84-95, 2008.

Stipendien und Auszeichnungen
  • Juli 2007 - Jan. 2009
  • Stipendiat nach dem Bayerischen Eliteförderungsgesetz (Universität Bayern e.V.)
  • Dez. 2008
  • Nachwuchsforscher-Preis der Universität Bayern e.V. (2. Preis)
  • Juli 2007 und Aug. 2008
  • Woody Bledsoe Travel Award