减速，靠边：自动驾驶责任敏感安全模型的正式验证、精化与测试案例研究
计算机科学中的逻辑
2023-05-16 v1 软件工程
系统与控制
系统与控制
摘要
技术进展开启了在无人类失误情况下驾驶、降低车辆排放并通过自动驾驶汽车未来简化日常任务的希望。确保这些车辆的安全对于该领域的延续至关重要。在本文中，我们形式化了自动驾驶汽车的责任敏感安全模型（RSS），并证明了该模型在纵向方向上的安全性与最优性。我们利用混系统定理证明器 KeYmaera X 将 RSS 形式化为具有非确定性控制选择与连续运动模型的混系统，并证明了碰撞的缺失。随后，我们通过精化证明展示了 RSS 的实用性，这些证明将已验证的非确定性控制包络转为确定性的，并进一步验证编译至 Python。精化与编译是保持安全的；因此，形式模型的安全性证明转移至编译后的代码，而在测试未验证模型的代码时所发现的反例也转移回形式模型。所得的 Python 代码允许在仿真中测试遵循 RSS 运动模型的汽车行为，利用源自形式模型的监视器度量模型与仿真之间的一致性，并将仿真中的反例报告回形式模型。
引用
@article{arxiv.2305.08812,
title = {Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars},
author = {Megan Strauss and Stefan Mitsch},
journal= {arXiv preprint arXiv:2305.08812},
year = {2023}
}