Schwammberger, Maike (2020) Distributed controllers for provably safe, live and fair autonomous car manoeuvres in urban traffic. PhD, Universität Oldenburg.

Preview

Volltext (2943Kb)

Abstract

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.

["eprint_fieldname_title_plus" not defined]

Verteilte Steuerungen für beweisbar sichere, lebendige und faire autonome Fahrmanöver im Stadtverkehr

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Autonomes Fahren, Stadtverkehr
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	17 Feb 2021 10:58
Last Modified:	17 Feb 2021 10:58
URI:	https://oops.uni-oldenburg.de/id/eprint/4961
URN:	urn:nbn:de:gbv:715-oops-50422
DOI:
Nutzungslizenz:

Actions (login required)

View Item