Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL

Albert Rizaldi, Jonas Keinholz, Monika Huber, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf, Tobias Nipkow

Publikation: Beitrag in Buch/Bericht/KonferenzbandKonferenzbeitragBegutachtung

60 Zitate (Scopus)

Abstract

Recent accidents involving autonomous vehicles prompt us to consider how we can engineer an autonomous vehicle which always obeys traffic rules. This is particularly challenging because traffic rules are rarely specified at the level of detail an engineer would expect. Hence, it is nearly impossible to formally monitor behaviours of autonomous vehicles—which are expressed in terms of position, velocity, and acceleration—with respect to the traffic rules—which are expressed by vague concepts such as “maintaining safe distance”. We show how we can use the Isabelle theorem prover to do this by first codifying the traffic rules abstractly and then subsequently concretising each atomic proposition in a verified manner. Thanks to Isabelle’s code generation, we can generate code which we can use to monitor the compliance of traffic rules formally.

OriginalspracheEnglisch
TitelIntegrated Formal Methods - 13th International Conference, IFM 2017, Proceedings
Redakteure/-innenSteve Schneider, Nadia Polikarpova
Herausgeber (Verlag)Springer Verlag
Seiten50-66
Seitenumfang17
ISBN (Print)9783319668444
DOIs
PublikationsstatusVeröffentlicht - 2017
Veranstaltung13th International Conference on Integrated Formal Methods, IFM 2017 - Turin, Italien
Dauer: 20 Sept. 201722 Sept. 2017

Publikationsreihe

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Band10510 LNCS
ISSN (Print)0302-9743
ISSN (elektronisch)1611-3349

Konferenz

Konferenz13th International Conference on Integrated Formal Methods, IFM 2017
Land/GebietItalien
OrtTurin
Zeitraum20/09/1722/09/17

Fingerprint

Untersuchen Sie die Forschungsthemen von „Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren