Automated Technology for Verification and Analysis 1st ed. 2020. Cham : Springer International Publishing, 2020 (2020), Seite 394-410 1 Online-Ressource(XIV, 574 p. 796 illus., 99 illus. in color.)
Während der letzten Jahre erobern autonome Fahrsysteme mehr und mehr die Märkte. Deshalb ist es insbesondere wichtig, zentrale Funktionen dieser Systeme sicherzustellen. Das Hauptanliegen dieser Doktorarbeit ist es, logische Schlussfolgerungen über Eigenschaften autonomer Fahrmanöver an innerstädtischen Kreuzungen zu ermöglichen. Hierfür werden ein Abstraktes Modell für Stadtverkehr-Netzwerke und die Verkehrs-Logik Urban Multi-lane Spatial Logic (UMLSL) eingeführt. Zudem werden als erweiterte Realzeitautomaten modellierte Kreuzungs-Controller vorgestellt, die UMLSL-Formeln für Abbiege-Manöver an Kreuzungen benutzen. Wir zeigen über logische Schlussfolgerungen die Sicherheit ("Kollisionsfreiheit") des Kreuzungs-Controllers und untersuchen die Lebendigkeit ("etwas gutes passiert irgendwann") und Fairness ("kein Vordrängeln") der Controller mit Hilfe des Model-Checking Tools UPPAAL. Als Fallstudie stellen wir zudem ein Kommunikations-Protokoll zum Warnen vor Unfällen vor.
While automated driving techniques are increasingly capturing the market, it is particularly important to consider vital functional properties of these systems. We introduce an approach to logically reason about functional properties of crossing manoeuvres at intersections. To this end, we introduce an abstract model for urban traffic situations and extended timed automata crossing controllers using formulae of our traffic logic Urban Multi-lane Spatial Logic (UMLSL) for turn manoeuvres at intersections. We show that even at complex intersections we can use purely spatial reasoning, detached from the underlying car dynamics, to prove safety (collision freedom) of the crossing controllers. We also examine liveness (something good finally happens) and fairness (no queue-jumping) of the controllers with the help of UPPAAL, a model-checker for (extended) timed automata. Furthermore, we introduce a case study, where we adapt the approach to a hazard warning communication protocol.
Fahrerassistenzsysteme werden immer autonomer und damit auch immer komplexer. Hier kann automatisiertes logisches Schließen für Verkehrsmanöver helfen, um solche Systeme zu analysieren. Multi-Lane Spatial Logic ist eine räumliche Logik, welche auf die Analyse von Verkehrsmanövern spezialisiert ist. Für diese Logik untersuchen wir Möglichkeiten der Automatisierung unter Berücksichtigung von ungenauen Sensordaten. Zusätzlich erweitern wir die Logik Duration Calculus mit der Möglichkeit temporale Präferenzen auszudrücken. Wir zeigen, dass Model Checking für ein relevantes Fragment der resultierenden Logik entscheidbar ist. Wir verbinden dies mit unserer Arbeit an Verkehrsmanövern, indem wir unsere Erweiterung verwenden, um ein Gefahrenwarnprotokoll für Autobahnen zu analysieren.
There is a trend in developing more and more autonomous driver assistance systems. Here, automation of formal spatio-temporal reasoning about traffic manoeuvres can help to analyse such systems. Multi-Lane Spatial Logic is a logic tailored towards formal reasoning about spatial aspects of motorways. For this logic we investigate means of automation, while paying special attention to imprecise information resulting from sensor readings. Additionally, we extend the logic Duration Calculus by introducing temporal discounting. We show that for a relevant fragment of our extension, model checking is decidable. We connect this to our work on traffic manoeuvres by using our extension to analyse the temporal quality of a hazard warning protocol for motorways.
Während der letzten Jahre erobern autonome Fahrsysteme mehr und mehr die Märkte. Deshalb ist es insbesondere wichtig, zentrale Funktionen dieser Systeme sicherzustellen. Das Hauptanliegen dieser Doktorarbeit ist es, logische Schlussfolgerungen über Eigenschaften autonomer Fahrmanöver an innerstädtischen Kreuzungen zu ermöglichen. Hierfür werden ein Abstraktes Modell für Stadtverkehr-Netzwerke und die Verkehrs-Logik Urban Multi-lane Spatial Logic (UMLSL) eingeführt. Zudem werden als erweiterte Realzeitautomaten modellierte Kreuzungs-Controller vorgestellt, die UMLSL-Formeln für Abbiege-Manöver an Kreuzungen benutzen. Wir zeigen über logische Schlussfolgerungen die Sicherheit ("Kollisionsfreiheit") des Kreuzungs-Controllers und untersuchen die Lebendigkeit ("etwas gutes passiert irgendwann") und Fairness ("kein Vordrängeln") der Controller mit Hilfe des Model-Checking Tools UPPAAL. Als Fallstudie stellen wir zudem ein Kommunikations-Protokoll zum Warnen vor Unfällen vor.
While automated driving techniques are increasingly capturing the market, it is particularly important to consider vital functional properties of these systems. We introduce an approach to logically reason about functional properties of crossing manoeuvres at intersections. To this end, we introduce an abstract model for urban traffic situations and extended timed automata crossing controllers using formulae of our traffic logic Urban Multi-lane Spatial Logic (UMLSL) for turn manoeuvres at intersections. We show that even at complex intersections we can use purely spatial reasoning, detached from the underlying car dynamics, to prove safety (collision freedom) of the crossing controllers. We also examine liveness (something good finally happens) and fairness (no queue-jumping) of the controllers with the help of UPPAAL, a model-checker for (extended) timed automata. Furthermore, we introduce a case study, where we adapt the approach to a hazard warning communication protocol.