Navigation

Contact

EMail: scare6sq@uol.deqc

DIRECTOR

Prof. Dr. Ernst-Rüdiger Olderog,

Department of Computing Science, FK II, University of Oldenburg,

D-26111 Oldenburg, Germany

oldegeirog@infmnormab5vtiohk.j/opunt4xli-olgzddenburg.d/vhex85

COODINATOR

Ira Wempe,

Department of Computing Science, FK II, University of Oldenburg,

D-26111 Oldenburg, Germany

ir9wa.wljemmpr/3pe@i0+pynnfo56rmmjktatikeai5f.uhbj/ni-be137oldenbrnkurg.dkxyekaom

Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL

Maike Schwammberger

Abstract

With Multi-lane Spatial Logic (MLSL) a powerful approach to formally reason about and prove safety of autonomous traffic manoeuvres was introduced. Extended timed automata controllers using MLSL were constructed to commit safe lane change manoeuvres on high-ways. However, the approach has only few implementation and verification results. We thus strenghen the MLSL approach by implementing their lane change controller in UPPAAL and confirming the safety of the lane change protocol. We also detect the unlive behaviour of the original controller and thus extend it to finally verify liveness of the new lane change controller.

Olivdo6snerr5mx Tam3he3cibel (oliv7tlfer.theedhjl@uauol.zu9rgde) (Changed: 2020-01-23)