User: Guest  Login
Original title:
Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL 
Translated title:
Formale Spezifikation, Erfüllbarkeitsanalyse, und formale Verifikation von autonomen Fahrzeugen in Isabelle/HOL 
Year:
2019 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Althoff, Matthias (Prof. Dr.) 
Referee:
Althoff, Matthias (Prof. Dr.); Nipkow, Tobias (Prof., Ph.D.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik; VER Technik der Verkehrsmittel 
Keywords:
formal specification, runtime monitoring, formal verification, manoeuvre automata, linear temporal logic, rechability analysis, traffic rules, concretisation, theorem prover, Isabelle 
TUM classification:
DAT 260d; DAT 815d 
Abstract:
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 u...    »
 
Translated abstract:
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...    »
 
Oral examination:
18.12.2019 
File size:
1218175 bytes 
Pages:
148 
Last change:
28.01.2020