Abgeschlossen am 28. März 2006 durch Baltin Karro.

• Prof. Dr.-Ing. Oliver Theel
• Dipl.-Inform. Jens Oehlerking
• Dipl.-Inform. Henning Burchardt
  

• Hybride Systeme
• Verifikation

Im Bereich der Regelung technischer Systeme spielt die Eigenschaft der Stabilität des Systems eine zentrale Rolle. Wann immer ein System durch Störeffekte in einen unerwünschten Zustand gebracht wird, soll automatisch dafür Sorge getragen werden, dass das System wieder in einen wünschenswerten Zustand zurückgebracht wird (d.h. sich stabilisiert). Beispiele für solche Systeme sind z.B. Heizungssysteme, Geschwindigkeitsregelungen an Fahrzeugen oder die Steuerung chemischer Prozesse. Solche Regelsysteme werden in der Regel durch Differentialgleichungen modelliert, und es exisiteren mathematische Methoden zum Stabilitätsnachweis.

Hybride Systeme sind eine spezielle Klasse von Regelsystemen, die sich dadurch auszeichnen, dass sie verschiedene Modi besitzen, in denen das System sich grundsätzlich unterschiedlich verhält. Aufgrund ihrer Flexibilität sind diese technischen Systeme von großem Interesse in Entwicklung und Forschung. Der Sonderforschungsbereiches AVACS, der dieser Arbeit zugrunde liegt, wendet Verifikationstechniken auf Systeme zur Steuerung und Regelung von Eisenbahnen an. Insbesondere soll ein Werkzeug zum automatischen Stabilitätsnachweis für solche Systeme entwickelt werden. Die existierenden Algorithmen für solche hybriden Systeme sind jeweils nur in der Lage, bestimmte Typen von hybriden Systemen zu verifizieren. Daher muss eine klassifizierung von Systemen in verschiedene Kategorien erfolgen.

Basierend auf gegebenen Spezifikationen hybrider Systeme soll ein Werkzeug entwickelt werden, dass eine Klassifizierung dieser Systeme anhand vorgegebener Kriterien vornimmt (zeitinvariant, konstant/linear in jedem Modus, deterministisch, lineare Schaltlogik). Hierzu müssen logische Formeln und Differentialgleichungen ausgewertet werden. Das Werkzeug soll leicht um weitere zu identifizierende Klassen erweitert werden können.

• Kenntnisse in C/C++
• Grundkenntnisse in Mathematik und Logik

Die Arbeit enthält praktische Anteile. Desweiteren ist die Möglichkeit gegeben, ggf. die Partneruniversitäten oder -institute innerhalb von AVACS (Universitäten Freiburg und Saarbrücken, Max-Planck-Institut Saarbrücken) zu besuchen.