TAP 2023
Tue 18 - Wed 19 July 2023 Leicester, United Kingdom
co-located with STAF 2023
Wed 19 Jul 2023 16:15 - 16:45 at Willow - TAP Session 6: Abstraction and Refinement Chair(s): Matteo Cimini

Technology advances give us the hope of driving without human error, reducing
vehicle emissions and simplify an everyday task with the future of self-driving cars. Self-driving cars have come a long way since their creation and making sure these vehicles are safe is very important to the continuation of this field. In this paper, we formalize the Responsibility-Sensitive Safety model (RSS) for self-driving cars and prove the safety and optimality of this model in the longitudinal direction. We utilize the hybrid systems theorem prover KeYmaera~X as a tool to formalize RSS as a hybrid system with both its non-deterministic control constraints and motion model, and prove absence of collisions. We then illustrate the practicality of RSS through refinement proofs that turn the verified non-deterministic controllers into deterministic ones and further verified compilation to Python. The refinement and compilation are safety-preserving; as a result, safety proofs of the formal model transfer to the compiled code, while counterexamples discovered in testing the code transfer back to the formal model. The resulting Python code allows to test the behavior of cars following the motion model of RSS in simulation, to measure agreement between the model and simulation with monitors that are derived from the formal model, and to report counterexamples from simulation back to the formal model.

Wed 19 Jul

Displayed time zone: London change

15:45 - 16:45
TAP Session 6: Abstraction and RefinementResearch Papers at Willow
Chair(s): Matteo Cimini University of Massachusetts Lowell

Remote Participants: Zoom Link

15:45
30m
Talk
Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion CheckingTAP Best Paper
Research Papers
P: Thibaut Benjamin Université Paris-Saclay, CEA, List, Julien Signoles Université Paris-Saclay, CEA, List
DOI
16:15
30m
Talk
Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars
Research Papers
P: Megan Strauss Carnegie Mellon University, Stefan Mitsch Carnegie Mellon University, USA
DOI