Verifikation und Simulation von selbst-optimierenden mechatronischen Systemen

Selbstoptimierende mechatronische Systeme passen ihre Software selbstständig ihrer veränderlichen Umwelt an. Dies wird auch als Rekonfiguration bezeichnet. Falls mehrere solcher mechatronischen Systeme miteinander interagieren, können sich zudem die Kommunikationsverbindungen und die Anzahl der Kommunikationspartner für ein System zur Laufzeit verändern. Um diese Systeme in sicherheitskritischen Umgebungen einsetzen zu können, muss eine korrekte Funktionsweise sichergestellt werden, um einen sicheren Betrieb zu ermöglichen.

Eine Möglichkeit, die Korrektheit des Systems bezüglich seiner Spezifikation sicherzustellen, ist eine modellgetriebene Entwicklung. Die ermöglicht den Einsatz formaler Methoden, die die Korrektheit des Systems beweisen. Die Integration der diskreten Softwareanteile mit den regelungstechnischen und mechanischen Anteilen des System kann mit simulationsbasierten Ansätzen überprüft werden.

In diesem Dissertationsprojekt werden Methoden und Algorithmen für die formale Verifikation und die Simulation von selbstoptimierenden mechatronischen Systemen entwickelt. Dabei ist es wichtig, dass die Verifikation die Rekonfiguration des Systems berücksichtigt, um korrekte Aussagen für das untersuchte System zu erhalten. Für die Verifikation wird das vollständige Systemverhalten auf zeitbehaftete Graphtransformationssysteme abgebildet, die dann mit einem Model Checking Ansatz verifiziert werden.

Die Simulation eines rekonfigurierbaren Systems wird von den Simulationswerkzeugen, wie z.B. Matlab/Simulink oder Dymola/Modelica, nicht direkt unterstützt. Um eine Simulation eines solchen System zu ermöglichen, muss im Rahmen dieses Projektes eine geeignete Kodierung des Modells für den Einsatz in einer solchen Simulationsumgebung gefunden werden.

Die in diesem Dissertationsprojekt erstellten Methoden und Algorithmen werden aufbauend auf der Fujaba Realtime Tool Suite implementiert.

Ansprechpartner: Christian Heinzemann