Formal Verification for ALICA Plans

Mit der Entwicklung von Wissenschaft und Technik steigen auch die Fähigkeiten autonomer Roboter. Immer mehr und kompliziertere Roboterszenarien werden in vielen Bereichen realisierbar, wie z. B. Mäh-, Ernte- und Lagerroboter. Daher wird die Planung für sie zu einer immer wichtigeren Aufgabe. Da diese Roboter jedoch täglich komplexer werden, ist die Sicherheitszertifizierung ein unvermeidliches Anliegen bei der Entwicklung von mehr autonomen Robotern. Daher ist die Verifizierung der Pläne vor der Verwendung und dem Einsatz der Roboter in der realen Welt derzeit eine der größten Herausforderungen. In dieser Arbeit präsentieren wir eine Lösung für die Verifikation von Multi-Agenten-Plänen, die mit der Sprache ALICA für mobile autonome Roboter spezifiziert sind. Als ersten Beitrag stellen wir den Algorithmus ALICA2UPPAAL vor. Basierend auf diesem Algorithmus wurde der Übersetzer, genannt A2U, entwickelt. Wir übersetzen und verifizieren die Pläne aus dem IMPERA-Projekt, um zu untersuchen, ob UPPAAL als Model Checker für ALICA-Pläne geeignet ist und nach der Übersetzung die Eigenschaft des ALICA-Plans beibehält. Experimente zeigen, dass der UPPAAL Model Checker nicht nur einen trivialen Fehler, sondern auch einen anspruchsvollen Fehler erkennen kann. Daher ist die Entwicklung von A2U unerlässlich. Außerdem stellen wir aufgrund des strukturellen Unterschieds zwischen dem ALICA-Plan und UPPAAL zwei Optimierungsmöglichkeiten für den Übersetzungsalgorithmus vor. Beide Optimierungen entfernen unnötige Transformationen aus einer Transformationssequenz und können in zukünftigen Arbeiten für andere Kontexte verwendet werden. Der letzte Beitrag ist eine Fallstudie zum Platooning von autonomen Fahrzeugen, die mit der A2U entwickelt wird. Die Fallstudie evaluiert die Fähigkeiten von A2U zur Übersetzung von zwei Modellen des autonomen Fahrzeugplatooning und die Fähigkeiten von UPPAAL zur Verifikation der komplexen Pläne. Die Untersuchung zeigt, dass A2U beide Modelle für autonomes Fahrzeug-Platooning übersetzen kann. Für das dynamische Modell sollten die Benutzer jedoch über Grundkenntnisse der UPPAAL-Modellprüfung verfügen, um die Pläne zu verifizieren und eine Zustandsraumexplosion zu vermeiden.