Statische und dynami... Studien- und Diploma... Statische und dynami...

Masterarbeit

Formale Verifikation relevanter Eigenschaften mittels CPN-Modellierung autonomer, kooperativer Roboter

 

Zusammenfassung

Im Rahmen des europäischen Projekts R3-COP wurde das Verhalten kooperierender, autonomer Robotik-Agenten mittels gefärbter Petri-Netze (CPN) modelliert, wobei missions- und umgebungsspezifische Informationen durch die jeweilige Anfangsmarkierung des Petri-Netzes erfasst wurden. Auf dieser Ebene wurden anschließend strukturelle Teststrategien definiert und umgesetzt.

Darauf aufbauend ist in dieser Master-Arbeit die Möglichkeit der Überprüfung vorgegebener Verhaltenseigenschaften durch formales Model Checking zu untersuchen. Hierzu sind zunächst sicherheits- bzw. nützlichkeitsrelevante Eigenschaften der modellierten Roboter-Fabrik zu definieren (etwa im Hinblick auf Kollisionsfreiheit, Terminierung bzw. begründeter Abbruch der Missionen, Verklemmungsfreiheit etc.) und formal zu erfassen. Insbesondere ist die Einsetzbarkeit der durch CPN Tools unterstützten Sprache ASK-CTL zu diesem Zweck zu bewerten und nach Möglichkeit zur Repräsentation und zur formalen Verifikation bzw. Widerlegung der zuvor ermittelten Eigenschaften zu verwenden.

Anschließend ist zu untersuchen, inwieweit sich übergeordnete Darstellungen des modellierten Verhaltens (bspw. mittels erweiterter Zustandsmaschinen) ermitteln lassen, die von speziellen missions- bzw. umgebungsspezifischen Markierungen nach Möglichkeit zu abstrahieren erlauben. Zweck dieser Darstellung ist die Vision, die verifikativen Ansätze künftig nicht mehr in Abhängigkeit von konkret vorliegenden Missions- bzw. Umgebungsfaktoren stets neu instanziieren zu müssen, sondern diese so generisch zu gestalten, dass sie (sei es durch Test oder durch Beweis) für ganze Klassen operationaler Randbedingungen die Gültigkeit der nachzuweisenden Eigenschaften einheitlich zu überprüfen erlauben.

Bearbeiter: Verena Held

Betreuer: Dr.-Ing. Matthias Meitner