Sichere Fahrstrategien durch formale Verifikation

Was heißt „Verifizieren“?

Beim autonomen Fahren reicht es nicht aus, ein Fahrzeug einfach möglichst viele Situationen ausprobieren zu lassen. Einzelne Tests können zwar Fehler finden, aber nicht beweisen, dass ein System unter allen möglichen Bedingungen sicher funktioniert. Gerade weil die Zahl möglicher Fahrsituationen praktisch unbegrenzt ist, braucht es Methoden, die über einzelne Testfälle hinausgehen.

Genau hier setzt die formale Verifikation an. Ein Modell wird dabei mathematisch darauf untersucht, ob bestimmte Eigenschaften für alle möglichen Entscheidungspfade gelten. So lässt sich überprüfen, ob unser Auto unter allen Umständen, die das Modell unterstützt, sicher fahren würde – ohne jeden möglichen Fall einzeln testen zu müssen.

Vom Fahrszenario zum Modell

Als Ausgangspunkt haben wir uns am Framework CommonUppRoad orientiert, das die beiden Tools UPPAAL für formale Modellierung und Verifikation sowie CommonRoad für die Darstellung und Simulation von Fahrszenarien miteinander verbindet.

Die Fahrszenarien werden zunächst mit CommonRoad beschrieben. Dabei werden unter anderem das Straßennetz, Hindernisse, der Initialzustand des Ego-Fahrzeugs und das Ziel festgelegt.

CommonUppRoad überführt diese Informationen anschließend in ein parametrisiertes UPPAAL-Modell bestehend aus mehreren synchronisierten zeitgesteuerten Automaten. Dabei wird die eigentliche Verhaltenslogik des Fahrzeugs ergänzt. Dadurch können unterschiedliche Szenarien mit demselben Modell untersucht, verifiziert und simuliert werden.

Visualisiertes Fahrszenario in CommonRoad (Grün: Startzustand, Rot: Statische Hindernisse, Gelb: Zielregion)

Parametrisiertes Modell in UPPAAL

Sicherheit zuerst, Optimierung danach

UPPAAL modelliert das Fahrszenario als eine Art Spiel, bei dem das Auto versucht zu gewinnen, indem es sein Ziel ohne Kollision erreicht. Dabei kann UPPAAL überprüfen, ob eine sichere Gewinnstrategie existiert.

Eine solche Strategie lässt sich vereinfacht als eine Anleitung für das Ego-Fahrzeug verstehen: Sie gibt vor, welche Entscheidungen das Ego-Fahrzeug in seinem aktuellen Zustand treffen darf, um garantiert sicher an sein Ziel zu gelangen.

Aktivierte Pfade ohne Strategie: Das Fahrzeug kann in eine unsichere Situation geraten.

Aktivierte Pfade unter Gewinnstrategie: Nur Entscheidungen, die eine sichere Weiterfahrt ermöglichen, werden zugelassen.

Damit ist zunächst die Sicherheit innerhalb des modellierten Seznarios garantiert. Erst danach kommt Machine Learning oder Reinforcement Learning ins Spiel. Innerhalb der durch die Strategie erlaubten Möglichkeiten wird nach einem möglichst guten Fahrmanöver gesucht, um Annäherung an das Ziel und Komfort mit ins Spiel zu bringen.

Kooperatives Fahren

Natürlich fährt kein Auto auf der Straße allein. Uns ist es also wichtig, auch kooperative Szenarien modellieren zu können. Es gibt jetzt also mehrere steuerbare Fahrzeuge, die wir in unsere Strategie einbeziehen müssen.

Das Problem bei dieser Sache ist, dass die Anzahl an möglichen Entscheidungssträngen bei einem Fahrzeug - und noch stärker bei mehreren Fahrzeugen - exponentiell wächst und irgendwann explodiert. Eine pauschale Lösung ist die Segmentierung von Szenarien, jedoch unter Verlust des Safety Shields und dem Aufkommen von Deadlocks bei der Zustandsübergabe an das nächste Segment.

Beispiel für einen Deadlock bei der Segmentierung eines Szenarios. Der Endzustand eines Segments ist der Anfangszustand des nächsten. Dieser Zustand kann zunächst sicher sein, jedoch dazu führen, dass im nächsten Segment keine initialen validen Fahrmanöver existieren.

Exponentiell wachsender Zustandsraum nach mehreren Simulationsschritten.

Die Zustandsraumexplosion ist damit eine der zentralen Herausforderungen, die wir an verschiedenen Stellschrauben angehen müssen.

Wo es weitergehen kann

Uns steht nun eine Grundlage zur Verfügung, um Fahrszenarien formal auf Sicherheit zu untersuchen und gleichzeitig gute Trajektorien zu erzeugen. Besonders interessant wird nun, wie sich die Methode auf komplexere Szenarien und kooperatives Fahren mit mehreren Fahrzeugen übertragen lässt. Dafür gilt es, die Zustandsraumexplosion als eine zentrale Herausforderung anzugehen.

Ebenfalls gilt es, die sicheren Strategien perspektivisch auf unsere Fahrzeuge zu bringen und diese tatsächlich danach fahren zu lassen.