以形式化方法为自动驾驶安全论证提供证据的路径

自动驾驶系统的安全性必须通过令人信服的论证加以证明，并以有力证据为支撑，以说服认证机构、监管实体及公众允许该系统上路。这种说服通常通过将对论证与有力证据汇编为安全论证（safety case）来实现。审查与测试是确保汽车系统正确性的两种常用方法，但无法穷尽探索通常无限的可能行为集合。相比之下，形式化方法是穷尽性方法，能提供模型正确性的数学证明，并可用于证明形式化的功能安全需求由系统组件的形式模型所满足。本文展示了形式化方法如何为功能安全需求向反馈环路中组件的正确分解提供证据，以及该证据如何契合安全论证的论证结构。若获得证明，形式模型即用作对组件的需求。这种安全论证结构可用于减轻对审查与测试的依赖以确保分解正确，从而节省数据收集与验证时间方面的开销。