Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL
Albert Rizaldi · mediaTUM – the media and publications repository of the Technical University Munich (Technical University Munich) · 2019
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: the notion of safe distance between an ego vehicle and its front vehicle, the framework for predicting the spatial occupancies of other traffic participants, the road networks in which autonomous vehicles shall operate, and relevant primitives required to detect lanes in which an autonomous vehicle currently occupies.Each of these elements are proved to be correct with respect to their own specification in the theorem prover isabelle, and refined to functions which are guaranteed to be correct numerically.Next, we formalise a collection of selected traffic rules from the German traffic code (Straßenverkhersordnung) and propose a method to monitor them formally.We translate the natural language requirements to formulas in linear temporal logic (LTL) without considering what each atomic proposition means initially.Then, we define the meaning of those atomic propositions precisely by using the previously formalised elements for formal analyses of autonomous vehicles.We monitor the satisfaction of a trace with respect to these formulas by executing the semantics of (finite-time) LTL implemented in the theorem prover isabelle.Lastly, we demonstrate how to use reachability analysis to formally construct a manoeuvre automaton which can be used for motion planning of autonomous vehicles; this construction involves a careful interaction with uncertified tools other than isabelle.Then, we propose a variant of LTL which is interpreted over sets instead of single trajectories because traces of manoeuvre automata will be sets (due to reachability analysis).We formalise a plan with this new specification language and then use satisfiability checking in conjunction with the previously formalised monitoring framework to search for a sequence of manoeuvres that is guaranteed to satisfy the plan.v Zusammenfassung 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: der Begriff des Sicherheitsabstands zwischen einem Ego-Fahrzeug und dem vorderen Fahrzeug, die Vorhersage der Straßenbelegung anderer Verkehrsteilnehmer, das Straßennetzwerk in dem autonome Fahrzeuge fahren sollen und relevante Primitive um Fahrspuren zu erkennen, die ein autonomes Fahrzeug momentan besetzt.Jedes dieser Elemente ist mit dem Theorembeweiser Isabelle als korrekt in Bezug zu deren Spezifikation bewiesen worden mit deren Hilfe Funktionen abgeleitet wurden, die numerische korrekt sind.Weiterhin wurde eine Menge an ausgewählten Verkehrsregeln der Straßenverkehrsordnung formalisiert und eine Methode vorgeschlagen, die deren Einhaltung formal überwacht.Die natürlichsprachigen Anforderungen wurden zu Formeln in linearer temporaler Logik (LTL) übersetzt ohne die ursprüngliche Bedeutung der Aussagenvariablen zu berücksichtigen.Als nächstes wurde die Bedeutung dieser Aussagenvariablen präzisiert, indem die zuvor formalisierten Elemente formaler Analyse autonomer Fahrzeuge herangezogen wurden.Die Einhaltung von Verhalten bezüglich dieser Formeln wird überwacht indem die im Theorembeweiser Isabelle implementierte Semantik von (zeitbeschränktem) LTL ausgeführt wird.Zuletzt wird die Verwendung von Erreichbarkeitsanalyse zur formalen Konstruktion eines Manöver-Automaten demonstriert, der zur Bewegungsplanung autonomer Fahrzeuge verwendet werden kann; dieser Ansatz erfordert ein sorgfältiges Zusammenspiel mit nicht-zertifizierten Werkzeugen neben Isabelle.Danach schlagen wir eine Variante von LTL vor, die über Mengen von Trajektorien interpretiert wird, anstatt über einzelne Trajektorien, da Verhalten von Manöver-Automaten sich nur durch Mengen beschränken vii lassen (aufgrund der Erreichbarkeitsanalyse). Ein Plan wird mit dieser neuen Spezifikationssprache formalisiert und anschließend wird eine Erfüllbarkeitsanalyse der Aussagenlogik zusammen mit dem vorher formalisierten Überwachungsframework ausgeführt, um eine Folge von Manövern zu finden, die den Plan garantiert erfüllt.viii