故障可运行汽车驾驶系统的形式化验证
软件工程
2021-02-10 v1 系统与控制
系统与控制
摘要
用于高度自动驾驶的故障可运行系统必须在发生故障时仍能完成驾驶任务。这需要冗余架构以及故障情况下重新配置系统的机制。因此，采用了仲裁逻辑。出于功能安全考虑，在任何电气和电子故障存在的情况下，必须切换到降级运行级别。为提供符合 ISO 26262 的安全论证证据，有必要对仲裁逻辑进行验证。验证过程确认了正确的故障反应，且不会达到非预期的系统状态。传统的安分析，如故障模式与影响分析，在这方面存在局限。我们提出了一种基于形式化验证（特别是模型检测）的分析方法，以验证驾驶系统的故障可运行行为。为此，我们对系统行为和相关架构进行建模，并形式化地规定了安全要求。分析范围根据 ISO 26262 的要求定义。我们验证了符合行业标准的高度自动驾驶故障可运行仲裁逻辑。我们的结果表明，形式化方法可成功应用于汽车故障可运行驾驶系统的安全评估。我们得以检测出其他分析会忽略的故障，从而有助于安全关键功能的开发。
引用
@article{arxiv.2101.07307,
title = {Formal Verification of a Fail-Operational Automotive Driving System},
author = {Tobias Schmid and Stefanie Schraufstetter and Jonas Fritzsch and Dominik Hellhake and Greta Koelln and Stefan Wagner},
journal= {arXiv preprint arXiv:2101.07307},
year = {2021}
}