Technology advances give us the hope of driving without human error, reducing vehicle emissions and simplifying an everyday task with the future of self-driving cars. 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 to formalize RSS as a hybrid system with its nondeterministic control choices and continuous motion model, and prove absence of collisions. We then illustrate the practicality of RSS through refinement proofs that turn the verified nondeterministic control envelopes 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 of an unverified model transfer back. 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.

翻译：技术进步让我们有望实现无人为误差的驾驶，减少车辆排放，并通过自动驾驶汽车简化日常出行任务。确保这些车辆的安全性对于该领域的持续发展至关重要。本文对自动驾驶汽车的“责任敏感安全模型”（RSS）进行了形式化处理，并证明了该模型在纵向方向上的安全性与最优性。我们利用混合系统定理证明器KeYmaera X将RSS形式化为混合系统，其中包含其非确定性控制选择和连续运动模型，并证明了无碰撞性。随后，我们通过精化证明展示了RSS的实用性：将已验证的非确定性控制包络转化为确定性控制包络，并进一步通过已验证的编译过程转换为Python代码。精化与编译过程均保持安全性不变；因此，形式化模型的安全性证明可传递给编译后的代码，而未经验证模型在代码测试中发现的反例则能反向传递回形式化模型。最终生成的Python代码支持在仿真环境中测试遵循RSS运动模型的车辆行为，通过从形式化模型派生的监控器衡量模型与仿真间的一致性，并将仿真中发现的反例反馈至形式化模型。