Formal Methods. FM 2019 International Workshops 1st ed. 2020. Cham : Springer International Publishing, 2020 (2020), Seite 249-264 1 Online-Ressource(XVIII, 523 p. 398 illus., 98 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.
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.
ACM/IEEE International Conference on Model Driven Engineering Languages and Systems (22. : 2019 : München) 2019 ACM/IEEE 22nd International Conference on Model Driven Engineering Languages and Systems companion Piscataway, NJ : IEEE, 2019 (2019), Seite 543-548 1 Online-Ressource