Formal Verification for ALICA Plans
| dc.date.accessioned | 2021-11-15T09:34:54Z | |
| dc.date.available | 2021-11-15T09:34:54Z | |
| dc.date.issued | 2021 | |
| dc.identifier | doi:10.17170/kobra-202111125069 | |
| dc.identifier.uri | http://hdl.handle.net/123456789/13383 | |
| dc.language.iso | eng | eng |
| dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 International | * |
| dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
| dc.subject.ddc | 004 | |
| dc.title | Formal Verification for ALICA Plans | eng |
| dc.type | Dissertation | |
| dcterms.abstract | 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. | ger |
| dcterms.abstract | Along with the development of science and technology, the capabilities of autonomous robots are increasing. An increasing number and their complication of robotic scenarios are becoming more viable in many domains, such as mowing, harvesting, and warehouse robots. Hence, planning for them becomes a more critical task. However, as these robots become more complex and encroaching daily, safety certification is an inevitable concern in the development of more autonomous robots. Therefore, the verification of the plans before using them and deploying the robots in the real world is currently one of the main challenges. In this work, we present a solution for the verification of multi-agent plans that are specified in the ALICA language for mobile autonomous robots. As the first contribution, we present an algorithm, namely ALICA2UPPAAL, and based on this algorithm, the translator, so-called A2U, was developed. We translate and verify the plans from our IMPERA project in order to examine whether UPPAAL is suitable as a model checker for ALICA plans and after translating the characteristic of the ALICA plan hold. Experiments show that the UPPAAL model checker not only can detect a trivial error but also a sophisticated error. Hence, the development of A2U is essential. Furthermore, due to the structural difference between the ALICA plan and UPPAAL, we present two optimization ways for the translation algorithm. Both optimizations remove unnecessary transformations from a transformation sequence and can be used in future work for other contexts. The last contribution is an autonomous vehicle platooning case study on the robotic automotive industry, which is developed with the A2U. The case study evaluates the capabilities of the A2U for translating two models of autonomous vehicle platooning and the capabilities of UPPAAL for verifying the complex plans. The research shows that A2U can translate both models for autonomous vehicle platooning. Still, for the dynamic model, in order to verify the plans and avoid state-space explosion, the users should have basic knowledge of UPPAAL model checkers. | eng |
| dcterms.accessRights | open access | |
| dcterms.creator | Nguyen Van, Thao | |
| dcterms.dateAccepted | 2021-10-21 | |
| dcterms.extent | xix, 110 Seiten | |
| dc.contributor.corporatename | Kassel, Universität Kassel, Fachbereich Elektrotechnik / Informatik | ger |
| dc.contributor.referee | Geihs, Kurt (Prof. Dr.) | |
| dc.contributor.referee | Thanh Vinh, Phan (Prof. Dr.) | |
| dc.subject.swd | Autonomer Roboter | ger |
| dc.subject.swd | Mehragentensystem | ger |
| dc.subject.swd | Planung | ger |
| dc.subject.swd | Verifikation | ger |
| dc.subject.swd | Übersetzer <Informatik> | ger |
| dc.subject.swd | Mensch-Maschine-Kommunikation | ger |
| dc.subject.swd | Fehlererkennung | ger |
| dc.type.version | publishedVersion | |
| kup.iskup | false | |
| ubks.epflicht | true |
Dateien zu dieser Ressource
Das Dokument erscheint in:
-
Dissertationen [21]
Solange nicht anders angezeigt, wird die Lizenz wie folgt beschrieben: Attribution-NonCommercial-NoDerivatives 4.0 International