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.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL ; Formale Spezifikation, Erfüllbarkeitsanalyse, und formale Verifikation von autonomen Fahrzeugen in Isabelle/HOL



    Erscheinungsdatum :

    28.01.2020


    Medientyp :

    Hochschulschrift


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Klassifikation :

    DDC:    000





    Absicherung sicherheitskritischer Systeme - formale Verifikation

    Tchernikov,M. / Swaminathan,M. | Kraftfahrwesen | 2009



    Formale Spezifikation und Verifikation von sicherheitskritischen Anlagen in der Bahntechnik mit SDL und MSC's

    Pansa, U. / Institut fur Automatisierungstechnik / Institut fur Regelungstechnik | British Library Conference Proceedings | 2000