Wintersemester 2013/14 und Sommersemester 2014
Projektgruppe Verifikation Hybrider Automaten
Modellierung und Verifikation von Service-Robotern
Prof. Dr. Bernhard BeckertSarah Grebing
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.
Ziel der Projektgruppe ist es, in Zusammenarbeit mit der Firma Bosch und der Arbeitsgruppe von Professor Platzer in Pittsburgh zu evaluieren, ob diese Technologie im Bereich autonome Navigation von mobilen Robotern Anwendung finden kann. Zudem sollen Konzepte zur Modellierung von der autonomen Navigation von mobilen Robotern entwickelt werden.
In der Projektgruppe sollen vorhandene Modelle eines autonomen Service-Roboters und die Beweise von Eigenschaften dieser Modelle nachvollzogen werden. Die Modelle sollen dann so erweitert werden, dass mehr Aspekte der Realität abgebildet werden und die Beweise von bestimmten Eigenschaften der Modelle sollen neu geführt werden. Es soll zudem der Begriff der "Sicherheit" in diesem System evaluiert werden und ggf. erweitert oder angepasst werden.
Bei Interesse bitte per E-Mail bei grebing melden. ∂mail informatik kit edu