Final published version
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Chapter (peer-reviewed) › peer-review
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Chapter (peer-reviewed) › peer-review
}
TY - CHAP
T1 - Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL
AU - Linker, Sven
PY - 2017/9/20
Y1 - 2017/9/20
N2 - Formal verification of autonomous vehicles on motorways is a challenging problem, due to the complex interactions between dynamical behaviours and controller choices of the vehicles. In previous work, we showed how an abstraction of motorway traffic, with an emphasis on spatial properties, can be beneficial. In this paper, we present a semantic embedding of a spatio-temporal multi-modal logic, specifically defined to reason about motorway traffic, into Isabelle/HOL. The semantic model is an abstraction of a motorway, emphasising local spatial properties, and parameterised by the types of sensors deployed in the vehicles. We use the logic to define controller constraints to ensure safety, i.e., the absence of collisions on the motorway. After proving safety with a restrictive definition of sensors, we relax these assumptions and show how to amend the controller constraints to still guarantee safety.
AB - Formal verification of autonomous vehicles on motorways is a challenging problem, due to the complex interactions between dynamical behaviours and controller choices of the vehicles. In previous work, we showed how an abstraction of motorway traffic, with an emphasis on spatial properties, can be beneficial. In this paper, we present a semantic embedding of a spatio-temporal multi-modal logic, specifically defined to reason about motorway traffic, into Isabelle/HOL. The semantic model is an abstraction of a motorway, emphasising local spatial properties, and parameterised by the types of sensors deployed in the vehicles. We use the logic to define controller constraints to ensure safety, i.e., the absence of collisions on the motorway. After proving safety with a restrictive definition of sensors, we relax these assumptions and show how to amend the controller constraints to still guarantee safety.
U2 - 10.1007/978-3-319-66845-1_3
DO - 10.1007/978-3-319-66845-1_3
M3 - Chapter (peer-reviewed)
SN - 9783319668444
T3 - Lecture Notes in Computer Science
SP - 34
EP - 49
BT - Integrated Formal Methods
A2 - Polikarpova, Nadia
A2 - Schneider, Steve
PB - Springer
CY - Cham
ER -