基于微分动态逻辑的自动驾驶安全形式化开发
系统与控制
2022-04-15 v1 系统与控制
摘要
为自动驾驶（AD）系统提供安全与正确行为的可信论证这一挑战，迄今阻碍了其广泛的商业部署。测试与仿真等传统开发方法受限于非穷尽分析，因而无法保证在所有可能场景下的正确性。形式化方法是一种利用系统模型提供正确性数学证明的途径，可用于给出必要的论证。本文研究了微分动态逻辑与演绎验证工具 KeYmaera X 在 AD 功能开发中的使用。具体地，给出了用于车道内 AD 功能的决策与控制模块不同设计变体的形式化模型与安全证明。在此过程中，识别了保证安全所需的假设与不变条件，并展示了此类分析如何在开发过程中协助需求精化与运行设计域的 formulation。此外，展示了如何在其所有允许行为中对不同模型的性能进行形式化穷尽分析。
引用
@article{arxiv.2204.06873,
title = {Formal Development of Safe Automated Driving using Differential Dynamic Logic},
author = {Yuvaraj Selvaraj and Wolfgang Ahrendt and Martin Fabian},
journal= {arXiv preprint arXiv:2204.06873},
year = {2022}
}