Proving Safety of Automated Driving Vehicles

I will introduce our recent work on using formal logic to rigorously prove the safety of automated driving vehicles. The main challenge in such formal verification attempts for real-world systems is the absence of target system models. We follow the methodology called RSS (responsibility-sensitive safety, Shalev-Shwartz et al., 2017) that tells what to model (and what not to model) in a both technically and socially sensible way. Our formalization and extension of RSS with a Floyd--Hoare-style program logic allows us to handle complex driving scenarios compositionally, and to cover real-world scenarios such as emergency pull over for the first time. I will demonstrate the use of obtained proofs with driving simulation. Overall, the work suggests the potential of formal logic as a social infrastructure for establishing trust in novel ICT. The talk is based on the following paper:

• Ichiro Hasuo, Clovis Eberhart, James Haydon et al. Goal-Aware RSS for Complex Scenarios via Program Logic. IEEE Trans. Intelligent Vehicles, to appear. [doi] [arxiv]

(The talk might not be especially long, perhaps 30-45 minutes.)

Zoom link: