This thesis combines three formal verification techniques — theorem proving, satisfiability checking (runtime monitoring), and reachability analysis — for formally analysing autonomous vehicles. First, we formalise the required elements which will be the foundation for formally analysing autonomous vehicles. Next, we formalise a collection of selected traffic rules from the German traffic code (Straßenverkhersordnung) and propose a method to monitor them formally. Lastly, we demonstrate how to use reachability analysis to formally construct a manoeuvre automaton which can be used for motion planning of autonomous vehicles. ; Diese Dissertation kombiniert drei Techniken der formale Verifikation - Theorembeweisen, Erfüllbarkeitsanalyse der Aussagenlogik und Erreichbarkeitsanalyse - um autonome Fahrzeuge formal zu analysieren. Zuerst werden die notwendigen Elemente formalisiert, die als Grundlage zur formalen Analyse autonomer Fahrzeuge dienen. Weiterhin wurde eine Menge an ausgewählten Verkehrsregeln der Straßenverkehrsordnung formalisiert und eine Methode vorgeschlagen, die deren Einhaltung formal überwacht. Zuletzt wird die Verwendung von Erreichbarkeitsanalyse zur formalen Konstruktion eines Manöver-Automaten demonstriert, der zur Bewegungsplanung autonomer Fahrzeuge verwendet werden kann.
Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL ; Formale Spezifikation, Erfüllbarkeitsanalyse, und formale Verifikation von autonomen Fahrzeugen in Isabelle/HOL
2020-01-28
Theses
Electronic Resource
English
DDC: | 000 |
Absicherung sicherheitskritischer Systeme - formale Verifikation
Automotive engineering | 2009
|Formale Verifikation von Spezifikations-Modellen
Tema Archive | 2001
|Formale Beschreibung und Verifikation von Hardwareprotokollen
Tema Archive | 1995
|British Library Conference Proceedings | 2000
|