Hybrid Systems Verification:
Autonome Navigation von mobilen Robotern

Typ:	BA
Datum:
Betreuer:	Bernhard Beckert
Aushang:

Systeme, die diskretes und kontinuierliches Verhalten kombinieren, können als "Hybride Systeme" modelliert werden. Eigenschaften dieser Modelle lassen sich dann mit Hilfe formaler Methoden nachweisen (verifizieren) und erlauben so Rückschlüsse auf das Verhalten des Systems.

Hybride Systeme erlauben eine Analyse des Designs von technischen Produkten in der Robotik, Automobilindustrie und in der Avionik. In diesen Gebieten spielen Systeme eine Rolle, die nicht nur Schaltungselemente enthalten, sondern auch physikalisches Verhalten wie Geschwindigkeit und Beschleunigung aufweisen. Zur Modellierung und Verifikation von hybriden Systemen existieren bereits einige Systeme, darunter auch das Verifikationswerkzeug "KeYmaera", entwickelt von Professor Andre Platzer.

In Zusammenarbeit mit der Firma Bosch und der Arbeitsgruppe von Professor Platzer in Pittsburgh soll am KIT evaluiert werden, ob diese Technologie im Bereich autonome Navigation von mobilen Robotern Anwendung finden kann. Die Master-/Diplomarbeit findet im Rahmen dieses Projekts statt und wird am KIT am Lehrstuhl von Professor Beckert betreut. Die Kooperation findet mit der Firma Bosch am Standort Schwieberdingen (bei Stuttgart) statt.

Aufgabenstellung:

Sie sollen sich in das Verifikationswerkzeug KeYmaera einarbeiten und sich mit der Modellierung und dem Nachweis von Eigenschaften von Hybriden System vertraut machen. Bereits existierende Modelle sollen von Ihnen auf Schwachstellen und Lücken analysiert und so verbessert werden, dass diese Schwachstellen und Lücken im Modell geschlossen werden. Ihre Ergebnisse sollen als Basis für eine Guideline dienen, die die Modellierung und die Verifikation mit KeYmaera beschreibt, um weitere Anwendungen mit KeYmaera zu verifizieren.

Ihre Kompentenzen:

• Sehr gute Studienleistungen
• Spaß am Lösen komplexer Probleme
• Interesse an formalen Methoden und deren Anwendungen, sowie Interesse, diese Methoden an realen Problemstellungen anzuwenden
• Kenntnisse im Bereich Modellierungs- und Verifikationstechniken
• Wünschenswert: Vorkenntnisse in KeYmaera und die in diesem System verwendeten Techniken

Das bieten wir Ihnen:

• Sie arbeiten an einer anspruchsvollen technischen Anwendung für Formale Methoden
• Sie bekommen Einblick in ein industrielles Forschungsprojekt
• Sie bekommen Einblick in ein führendes Technologie- und Dienstleistungsunternehmen
• Eine internationale Kooperation mit der Möglichkeit der Teilnahme im interACT Programm

Bei Fragen oder Interesse melden Sie sich bitte bei Professor Beckert (beckert@kit.edu).