« zurück

Erfolgreiche Verteidigung der Dissertation

Dr. Tim Meywerk

Dr. Tim Meywerk hat seine Dissertation " Modelling, Verification and Test of High-level Robotic Plans" erfolgreich verteidigt.

Roboter sind ein integraler Bestandteil aktueller industrieller Prozesse. Typische industrielle Roboter werden an verschiedenen Stellen in Fabriken eingesetzt, um repetitive Aufgaben zu bearbeiten und so das Arbeitspensum menschlicher Arbeiter zu verringern. Durch technologische Fortschritte, vor allem im Bereich künstlicher Intelligenz, wird der Weg für eine neue Generation mobilerer und flexiblerer autonomer Roboter geebnet, die für eine größere Menge von Anwendungen eingesetzt werden können. Die Kombination aus dynamischen Umgebungen, komplexen Aufgaben und dem Bedürfnis, das Verhalten der Roboter erklären zu können, verlangen nach einem strukturierten, abstrakten Ansatz zur Steuerung autonomer Roboter. Ein solcher Ansatz ist die planbasierte Robotik, in der ein abstrakter Plan für die Koordination und Überwachung kleinerer Module wie etwa eines Bewegungsplaners, einer Wissensdatenbank oder eines Bilderkennungsmoduls verantwortlich ist. Der Plan selbst ist in einer abstrakten Plansprache geschrieben.

Mit der steigenden Komplexität der robotischen Pläne werden Programmier- und Flüchtigkeitsfehler immer wahrscheinlicher. Es gibt einen unbestreitbaren Bedarf an einem hohen Grad von Sicherheit, Robustheit und Korrektheit der autonomen Roboter. Hierzu ist nicht nur eine sorgfältige Entwicklung der Software des Roboters nötig, sondern auch Techniken, um die Korrektheit zu beurteilen und versteckte Fehler aufzudecken. Diese Dissertation zielt darauf ab, den Stand der Forschung im Bereich der Verifikationstechniken für abstrakte Roboterpläne wesentlich zu erweitern. Hierzu werden sowohl formale als auch test-basierte Methoden vorgestellt. Insbesondere werden Beiträge zu den folgenden drei Themengebieten der robotischen Planverifikation geleistet. Der erste Beitrag umfasst mehrere Techniken zur symbolischen Verifikation von abstrakten Roboterplänen, der zweite ist die Entwicklung von zwei Ansätzen, die bei der Modellierung von robotischen Umgebungen unterstützen und somit sowohl den Planungs- als auch den Verifikationsprozess erleichtern und zuletzt wird abdeckungsgetriebenes Fuzzing als eine automatische, testbasierte Methode zur Fehlerfindung in robotischen Plänen vorgestellt. Alle vorgestellten Beiträge werden auf die CRAM Plan Language (CPL) angewendet. Sie werden in dieser Dissertation im Detail erläutert und experimentell evaluiert, um ihre Wirksamkeit zu demonstrieren.

Wir gratulieren!