论文标题

使用不同动态逻辑的安全自动驾驶的正式开发

Formal Development of Safe Automated Driving using Differential Dynamic Logic

论文作者

Selvaraj, Yuvaraj, Ahrendt, Wolfgang, Fabian, Martin

论文摘要

到目前为止,为自动驾驶系统的安全和正确行为提供令人信服的论点(到目前为止)所面临的挑战阻碍了他们广泛的商业部署。常规的开发方法(例如测试和仿真)受到非排量分析的限制,因此不能在所有可能的情况下保证正确性。正式方法是一种使用系统模型提供数学证明的方法,可用于提供必要的参数。本文研究了在AD功能的开发中使用差异动态逻辑和演绎验证工具keymaera X。具体而言,提出了针对车道上广告特征的决策和控制模块不同设计变体的正式模型和安全证明。在此过程中,确定了确保安全性所需的假设和不变条件,并且本文显示了在开发过程中,在需要改进和制定操作设计领域的过程中,这种分析如何有所帮助。此外,在其所有允许的行为中,如何对不同模型的性能进行正式分析。

The challenges in providing convincing arguments for safe and correct behavior of automated driving (AD) systems have so far hindered their widespread commercial deployment. Conventional development approaches such as testing and simulation are limited by non-exhaustive analysis, and can thus not guarantee correctness in all possible scenarios. Formal methods is an approach to provide mathematical proofs of correctness, using a model of a system, that could be used to give the necessary arguments. This paper investigates the use of differential dynamic logic and the deductive verification tool KeYmaera X in the development of an AD feature. Specifically, formal models and safety proofs of different design variants of a Decision & Control module for an in-lane AD feature are presented. In doing so, the assumptions and invariant conditions necessary to guarantee safety are identified, and the paper shows how such an analysis helps during the development process in requirement refinement and formulation of the operational design domain. Furthermore, it is shown how the performance of the different models is formally analyzed exhaustively, in all their allowed behaviors.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源