24年11月来自意大利Modena大学的论文“Open Challenges in the Formal Verification of Autonomous Driving”。
在自动驾驶领域，开发和集成高度复杂和异构的系统是标准做法。现代车辆不是单片系统；而是由不同的硬件组件组成，每个组件都运行自己的软件系统。自动驾驶汽车由许多独立的组件组成，这些组件通常由不同的、可能相互竞争的公司开发。这种多样性给认证过程带来了重大挑战，因为它需要认证可能不会泄露其内部行为（黑匣子）的组件。本文介绍一个自动驾驶系统的真实案例研究，确定了与其开发和集成相关的关键开放挑战，并探讨了形式化验证技术如何应对这些挑战以确保系统的可靠性和安全性。
如 [27] 所述，美国汽车工程师协会 (SAE) 将自动驾驶的设计目标定义为六个不同等级，从 0 级 (L-0) 到 5 级 (L-5)。这些等级代表了自动化的一个范围：L-0 表示无自动化，L-1 表示有驾驶辅助，L-2 表示部分自动化，L-3 表示有条件自动化，L-4 表示高度自动化，最高的 L-5 表示完全自动化。每个等级都反映了自动驾驶系统不断增强的能力及其与人类驾驶员的交互。目前，大多数商用汽车都处于 L-2 自动化水平。这一级别包含自适应巡航控制和车道保持辅助等功能，使汽车能够协助驾驶员，同时仍需要持续的监督和主动参与。一些制造商正在探索 L-3 系统，该系统在特定情况下提供有条件的自动化。例如，一些配备了 L-3 系统的现代车辆可以自动驾驶高速公路，包括车道保持、速度调节和自适应巡航控制，但在驶出高速公路或在复杂的城市环境中行驶时需要驾驶员接管。尽管取得了这些进步，但该行业仍处于全面实施更高水平自动化的早期阶段。
根据最近关于该主题的调查 [17]，实现 L-5 自主性需要适当整合技术和高效的通信渠道。要充分发挥自动驾驶的潜力，需要可靠、强大且广泛的移动网络。本文的兴趣是如何使自动驾驶的组件及其交互更加可靠。为了实现这一目标，从现实世界的自动驾驶系统的案例研究开始，并从形式化的角度解决提高其可靠性的问题。
在自动化用例中部署智能需要两个关键组件：强大的计算硬件和众多传感器模块，以便及时准确地解释周围环境和车舱内环境。这对汽车工程师来说是一个重大挑战，他们必须将 TOPS-算力贪婪软件组件集成到节能电路板上，理想情况下，这些电路板应具有多核数据处理器，例如 NVIDIA Orin [25] 或 AMD XILINX [7, 1] 的处理器。如图展示下一代 ECU 的目标架构。
这些系统采用多核主机平台，包括实时和非实时核心 ISA（指令集架构），定义处理器可以执行的指令集。这些指令集与数据处理架构（如 GPGPU [25]、可重构阵列 [1]）或专用电路相结合，以直接在硬件中实现处理算法。如此复杂的架构带来了两个主要挑战。
1 不可信组件的异构组合
第一个挑战涉及管理具有不同可靠性级别的组件。一些组件是开源的（白盒），允许完全访问和修改，而另一些组件是闭源的（黑盒），限制对其内部工作的访问。为了应对这一挑战，利用形式化验证技术。具体而言，如 [20] 中所述，采用形式化验证方法，重点关注三个关键领域（也称为配方）：决策组件的验证、基于 AI 的组件以及安全声明的执行。
2 映射分布式计算的有效策略
应对这一挑战需要使用形式化验证技术来确保映射策略既高效又可靠（因为处于实时系统中）。可以使用形式化验证系统地验证软件组件是否在计算核心中以最佳方式分布，以及冗余和投票机制是否正确实施以增强容错能力和系统稳健性。通过形式化验证这些策略，可以保证系统满足其性能和可靠性要求，即使在存在组件故障或不确定性的情况下也是如此。事实上，包含冗余和投票方案的容错设计在减轻组件故障的影响方面发挥着至关重要的作用。[9] 中提出的研究为使用形式化验证技术来验证这些设计的正确性提供了宝贵的见解。通过系统地验证容错硬件是否满足指定的可靠性要求，证明了形式化方法在识别传统测试可能忽略的设计错误方面的有效性。
虽然形式化方法（FM）为在自主系统中集成异构组件和高效映射提供了一种有前途的方法，但它们的使用存在重大的实际限制。主要挑战包括对专业知识的需求、可扩展性问题、结果的可解释性、处理不确定环境的困难以及开发中的成本效益权衡。
一个关键限制是进入门槛高，因为 FM 通常需要
形式逻辑和验证技术
方面的深厚专业知识。这种专业技能在标准工程团队中并不常见，而且指定和验证系统的过程可能非常耗时。尽管开发了旨在使 FM 更易于访问的新工具，但它们的功能仍在不断发展，并且通常需要进行大量改进才能满足行业需求。
可扩展性和复杂性
也是主要障碍。自主系统由众多相互作用的组件组成，导致状态空间呈指数增长，使得详尽的验证在计算上成本高昂或不可行。组合推理和模块化验证等技术试图管理这一点，但它们需要仔细的抽象，这可能会过度简化或忽略关键行为。此外，模型检查可能需要大量计算，尤其是在应用于实时或资源受限的系统时，而假设-保证推理取决于准确的假设，而这些假设在实践中很难保证。
