点击上方“3D视觉车间，选择星标
干货第一时间送达
作者丨Penny@知乎
来源丨计算机视觉深度学习和自动驾驶
arXiv2022年2月6日上传的综述论文Automated Vehicle Safety Guarantee, Verification and Certification: A Survey作者来自俄亥俄州立大学。
与自动驾驶相关的挑战不再仅仅集中在自动驾驶汽车上（AV）在制造方面，在确保其运行安全方面。L3级和L4级独立驾驶的最新进展促使人们复杂AV对机动安全保障进行了更广泛的研究ISO2148(即预期功能安全)SOTIF）目标一致，即尽量减少已知和未知的不安全场景，以及零死亡（VZ）-到2050年消除公路死亡事故。
为AV运动控制提供安全保障的大多数方法都来自于形式（formal）方法，特别是可达性分析（reachability analysis，RA），它依赖于系统动态演化的数学模型来提供保障。本文总结了安全检查和确认（safety verification & validation）和认证过程（certification process），并回顾了最合适的AV的形式（formal）安全技术。 作者提出了统一的场景覆盖框架，它可以为自动驾驶汽车提供一种形式（formal）或 基于样本（sample）安全验证评估。最后，是AV挑战安全保障和未来机遇。
以往对自动驾驶技术的总结一直集中在感知、决策、车辆控制、人机交互执行等技术挑战和实施的各个方面，以及一些涉及自动驾驶安全验证和确认的总结（V&V）问题。
随着现实世界中自动驾驶系统的部署，现实世界中场景的规模需要大量的验证和确认。最大化场景覆盖率的常见验证和确认策略是在虚拟仿真中验证和模拟大量生成的场景样本。
基于场景采样V&V，挑战是量化可以保证样本量的合理覆盖，从而约束自动驾驶不当驱动造成的风险。合理的场景覆盖保证也是最近高度自动驾驶汽车（HAV）立法认证的先决条件。然而，另一组基于形式验证（formal verification）通过规范满意度的方法（ specification satisfaction）以不同的方式解决场景覆盖问题。由于形式（formal）新兴研究究方面的潜力，新兴研究已经开始形式属性（formal properties）与控制合成（control synthesis）和安全验证（safety verification）相结合。
鉴于自动驾驶量化验证的需要，提出了统一的场景覆盖框架，解决自动驾驶场景覆盖未解决的困难。可接受单个场景(基于样本的方法)的覆盖表示量或形式（formal）所谓安全规范规范（specification penetration rate）该框架定量定义了统一的安全场景覆盖率。定量定义将基于样本的方法和形式（formal）该方法结合在一起，为安全验证提供场景覆盖。候选自动驾驶车控制策略可以通过形式进行（formal）或基于样本的安全验证，指定ODD（operation defined domain）场景测试其安全场景覆盖率。作者比较了样本的方法和形式（formal）该方法的优缺点是基于如何实现该安全覆盖率，以及该方法的相关成本和争论。
下表是自动驾驶立法的现状：
在所有相关问题中，自动驾驶安全认证面临四个特殊挑战：
确定不可避免的碰撞；
责任确定；
合理场景覆盖验证成本；
重新验证自动驾驶系统更新的额外成本。
这不仅是一个学术问题，也是一个与责任有关的法律问题。尽管人们对自主性有很高的期望，但作为人类，只能期望机器人系统优化行动以获得最佳结果。例如，人们只能期望自动驾驶车辆采取避免不可避免碰撞的策略。关于这种可避免性确定的要求，HAV中的L3级到 L2021年8月，德国法律修正案通过了4级功能。
配备自动驾驶功能的机动车必须具备能够独立遵守车辆驾驶交通法规的技术设备和事故预防（accident prevention）系统包括：
（a） 旨在避免和减少损害，
（b） 如果不同的法律利益不可避免地受到损害，保护人的生命是最高优先事项
（c） 若有不可避免的人生选择风险，则无需根据个人特点进一步加权。
责任确定（liability determination）部署自动驾驶系统是一个需要解决的新问题。在L3级，只要事故或困难提前移交给司机，自动驾驶系统不承担责任，因为它只需要有限ODD确保环境安全。即使人类司机没有及时接管，自动驾驶系统的责任也可以在一定程度上免除，如制动、停车和打开危险灯。当L4级以上自动驾驶车辆配备形式安全验证时，可根据形式逻辑进行验证（formal logic）简化责任确定，如下图所示：基于样本安全验证开发的自动驾驶系统尚不清楚如何确定类似的程序执行形式。
广泛使用的安全指南标准ISO 26262道路车辆功能安全只适用于缓解与已知部件故障（即已知不安全）相关的已知不合理风险，但不解决复杂环境变量造成的自动驾驶风险，以及自动驾驶系统如何应对这些风险，此时车辆无技术故障。
鉴于上述安全挑战，ISO 21448提出了自动驾驶功能设计的已知和未知不安全场景结果最小化的定性目标（goals），如图所示：
然而，实现这一点SOTIF目标的挑战是现场操作测试等传统方法（field operational test），很难涵盖测试期间自动驾驶的所有可能场景。尽管存在挑战，但在安全分析方面仍有一些有前途的方法和方向，可以朝向ISO 21448的目标，如在模拟测试中最大限度地扩大场景覆盖率，或通过形式（formal）创造安全保障的方法。
在技术术语中，足够安全通常表示指定ODD完整或足够的场景覆盖范围。事实上，现有法律法规的要求相对较弱，只需检查一些关键场景。
在离散场景周围介绍δ-为场景样本分配量是一种很有希望的尝试。T-wise通过巧妙选择样本有限的候选人，可以实现几乎所有的数学算法，如泊松过程（almost full）统计覆盖。
乐观地假设，这种定量覆盖表明问题已经在整个社区得到了解决和接受，每个采样场景都有一个覆盖（coverage volume）。然后，基于样本方法的完整场景覆盖任务将进行足够数量的样品验证测试，以确保每个覆盖单元与至少一个安全测试结果相关。
事实上，一些场景空间的存在可能不会产生安全测试结果（例如，与障碍物的反应距离太小）。在这种情况下，需要额外的努力来确认这些场景是不安全的。在类型审批和认证方面，当权人需要设定一个可接受的成功门槛，以满足公众的期望。最简单的阈值是确认不同的安全测试数量和ODD场景测试所需的最小测试数量比。
在自动驾驶开发阶段，多样化的测试场景采样是加强安全控制的主要方法之一。尽量减少已知和未知的不安全场景SOTIF在优化目标方面，基于样本的方法在发现未知的不安全场景方面有更少的偏差和更多的探索能力。从未知到已知的推广是水平的，即所有采样场景通常处于相同的模拟环境和相同的真实性水平。
如图所示，正式方法与基于样本的方法之间的场景覆盖率比较：正式方法从更抽象层的安全规范开始，场景空间可能有更大的单一覆盖，但正式规范集成到控制合成或监控过程，可能依赖于控制器数学，繁琐；由于随机生成过程，基于样本的场景覆盖范围更加分散，但直接从模拟层覆盖，这使得采样过程简单易行。这两种方法都试图将验证场景投射到真实驾驶中，但模拟层和真实驾驶之间的差异总是存在的。
与基于测试的安全验证和保证方法相比，形式（formal）由于其严格的逻辑基础，该方法具有较高的陈述可靠性。
常用的自动驾驶汽车安全形式（formal）该方法包括模型检查、可达性分析和定理证明。模型检查起源于软件开发，以确保软件行为符合设计规范。当安全规范用公理和引理时（axioms & lemmas）假设情况下的安全性可以通过定理证明来验证。可达性分析在这三种分析中占有特殊地位，因为它具有为动态系统生成安全陈述的固有能力，能够捕捉的主要特征。
现实世界的道路测试或现场操作测试（FOT）自动驾驶汽车的验证和确认（V&V）最后一步也是昂贵的方法。从某种意义上说，这是验证的唯一途径。然而，FOT缺点也很明显：当安装候选自动驾驶控制器时，它缺乏足够的场景覆盖能力（特别是接近碰撞和碰撞的场景）。如图所示，基于样本和形式（formal）现场操作测试（FOT）比较方法：得分为0-10分，10分代表最高满意度。
形式化（formal）方法是一类应用数学中的严格技术（通常以逻辑计算的形式）来实现软件和工程设计规范和验证的方法。根据定义，它在安全验证任务中具有固有的优势，但具有连续动态的高系统复杂性一直是其在自动驾驶广泛应用的主要限制因素，即扩展性造成的困难。从技术上讲，形式化（formal）方法可以概括为一个实现或者转换抽象规范为系统控制算法/程序的过程，这样受控的系统行为可以满足所述的规范。
定义的动态系统：
最大前向可达集（Maximal Forward Reachable Set）定义如下
前向可达集（FRS）传播动态，自初始时间t0起，到未来时间t内的所有可能可达状态。
相反，后向可达集（BRS）的后向传播，查找来自前一时间t的所有可能状态，其导致当前时间t0达到某个目标状态集Xgoal，即如下最大后向可达集（Maximal Backward Reachable Set）的定义
另外，最小BRS定义为：
某些情况下，定义时间范围内的可达性更令人感兴趣。因此，把定义扩展到包括从当前时间到时间范围结束，比如最大前向可达集的定义修正为（其他类推）：
当不同交通参与者之间的交互起着关键作用时，必须将参与有时甚至是对抗智体的影响纳入可达性分析。在这种情况下，动态系统要引入额外的输入d，以表示这种对抗性控制输入：
这样的话，系统中对抗性输入的影响不取决于自车控制，因此必须保守建模，以便在最坏的情况下提供安全保证。
如下是进一步限制在对抗影响下最大FRS的定义：
在计算机科学和机器人技术领域，信号时域逻辑（STL）是一种通用语言，用于表达和指定时间紧要且包含连续变量的需求。如下表列出STL的基本语义。简言之，STL使用一阶逻辑（定义为，一组在非逻辑目标如变量采取量化的形式化系统）对变量的时域发展进行说明。
如下表是基本的STL语义：
自动驾驶车的示例性临时安全规范可以是“永远不会在交通中造成碰撞”，但一旦转换为STL规范，临时规范中的一些模糊之处需要消除。首先，“原因”一词在STL中没有得到很好的定义，因为它涉及碰撞责任认定（liability determination）的复杂性，可能必须用“处于”一词替换，这是一种责任中立的说法。然后，临时规范变成了“永远不要处于交通中的碰撞”。其次，STL要求规范有一个精确定义的时间范围，对于自动驾驶来说，通常使用时间范围的概念将时间跨度缩小到一个实用且可处理的水平。因此，临时规范可以进一步修改为“永不（在时间范围内）处于冲撞中”。
上述STL翻译的安全规范在集合语言中仍然停留在抽象层面，自动驾驶车控制算法设计师有责任把规范合成到控制器架构，或对设计的控制器进行安全验证，有足够的信心或确凿的证据确保其满足规范。
除了控制合成之外，STL表达的安全规范，可以在控制器原型设计期间用作主张，来指明安全违规行为，因此开发人员在控制设计期间要不断了解安全规范。确定安全规范的逻辑计算，通常通过解决一种决策的满足模理论（satisfiability modulo theory，SMT) 问题，来完成。
基于采样的方法，通过填充大量场景样本来验证场景变化。与基于采样的方法不同，主要是在控制器中实现安全规范，在环境模拟中达到一定的逼真度。这是由于验证安全的机制不同。在形式化的安全哲学中，安全规范要么得到满足，要么被违反，把规范的满足合成到基于模型的控制设计中。这样设计完成后，在运行过程中确保实现的责任转移到模型正确性的在线验证上：只要面向控制的模型验证为正确的，控制器按照综合安全规范执行，那么系统就可以证明是安全的。
在不丧失普遍性的情况下，安全规范φ，在某些情况下可能不可行（例如不可避免的碰撞），∀u，（s，t ）/|= φ。在这种情况下，φ-综合控制器，无法找到一个可行的控制序列来实现φ，最好的做法是，将情况提升到有预谋的紧急情况或应变策略（如碰撞冲击准备）。在任何情况下，由于设计的φ-合成控制器，已经用尽了其可用的动作，仍然无法找到φ-满足的动作，所以对于不可避免的损坏，控制器不算故障错误。
根据ISO 21448，场景（scenario）是一系列情景（scene）中几个情景之间时域发展的描述，情景是环境的快照，包括景色（scenery）、动态元素、所有参与者和观察者的自表征，以及这些实体之间的关系。根据这一定义，确保在定义的OOD中完全安全的任务可以描述为，对ODD所有可能场景变化进行安全验证和确认（V&V）。ODD中场景变化有两个方面：初始场景的变化，以及自初始场景以来时域发展的变化。场景变化的不同维度如图所示：
基于样本的方法并不显式地拥有与每个样本场景相关联的体量属性，因为每个场景样本都是基础的，并且体量较小。为了对两种安全验证方法进行统一比较和利用，必须将场景体量（scenario volume）的概念分配给基于样本的方法。为简单起见，假设所有N个连续维度彼此正交，并为参数组指定的场景样本，分配一个N-维场景空间的轴对齐多边形体量「p01，p02，...，p0N」。
在基于样本的方法中，在每个场景样本检查模拟场景的安全性。另一方面，形式化方法，通常在执行任何仿真之前，先从安全规范开始，然后将规范翻译成机器可理解的语言声明，例如或。然后，应用翻译的规范，可以通过在模拟/真实世界测试中检查规范的有效性，或者在控制合成期间将规范转换为系统约束或其他控制设计功能。
理想情况下，对于形式化方法，如果所有与安全相关的规范首先被真实地转化为此类机器可理解的陈述，并且如果综合控制器完全尊重这些陈述，并使用基于模型的控制器对（模拟）环境进行完美建模，那么场景覆盖率相对于模拟层是100%。 例如，表达式“自动驾驶车辆应始终无碰撞”可以转换为数学函数形式的可验证表达式，该数学函数评估自动驾驶车辆与仿真模型中任何其他目标之间的占用重叠，如果仿真中发生重叠，则返回true。
然而，由于以下原因，实际挑战阻碍了形式化安全规范的100%理想翻译：
首先，形式化方法依赖于基于现实世界抽象的观点，因此抽象和现实之间的差异（无论大小）将发生，并损害有效的安全保障。
第二，实际开发的控制器通常有性能限制，在任何情况下都无法符合安全规范。
第三，当形式化安全规范转换为安全验证或控制综合时，存在实际的可扩展性困难。换句话说，形式化方法在现实的穿透率通常低于100%。在形式上，穿透率定义为：形式化安全规范规定的场景子空间中可验证场景的百分比。
实际上，在指定的ODD中找出自动驾驶车候选控制器的规格穿透率可能是一个挑战。首先，定理证明等演绎形式化（deductive formal ）方法仅限于相对简单的离散动态系统，将定理证明扩展到连续动态系统需要进一步建立框架和相当高的计算资源。其次，传统的算法形式化（algorithmic formal ）方法，如模型检查，也不适用于连续动态系统，当需要对连续动作空间进行精细离散化时，所有可能动作进行穷举测试也会产生计算资源问题。然而，将STL与可达性分析相结合的最新进展，可以通过计算ODD场景空间中候选控制器的验证算术（verification arithmetic）来评估这种穿透率，并预测候选控制器不符合STL规范的体量部分。规范穿透率计算问题仍然是一个开放的问题，未来的工作可能会结合不同的证据收集方法，包括演绎和算法，提供不同的替代方案。
完成场景覆盖的路线如图所示：形式化方法和基于样本的方法都是帮助发现自动驾驶车安全控制弱点的有效工具，自动驾驶车的控制开发者可以根据自己的便利性和偏好选择其中一种或两种方法。
该图实际上是安全验证的控制政策演变示意图。在（a）-（e）中，形式化方法从ODD（a）的安全规范开始，然后进行初始安全规范穿透测试，查看安全规范保持得有多好（b）。然后执行可行性检查，以查看有多少失败的场景实际上是安全可行的（c）。然后重新设计自动驾驶车的控制器，以修复故障场景量区域（d），最终用候选自动驾驶车控制器验证所有安全可行场景量的安全性。在（f）-（j）中，基于样本的方法首先将ODD分割为可验证的场景单元（f），然后执行不完整的采样安全测试，检查候选自动驾驶车控制器（g）的主要问题。随后进行完全饱和采样，以确保场景覆盖率（h）。在全场景覆盖测试之后，控制器的弱点被暴露出来，重新设计过程将重复（i）。最终，控制器的弱点停止减少，控制器重新设计过程可能结束（j）。请注意，通过形式化方法，可以确定安全不可行的场景区域，并且一旦验证了ODD中除安全不可行场景体之外的所有体量，就不需要进行进一步重新设计。
安全验证可以在模拟仿真期间（在线）用预测模块执行，也可以在模拟仿真之后（离线）执行，简单地检查结果，如图所示即不同验证方案概览：
当自车和参与交通智体的控制策略已知（白盒控制）或部分已知（灰色控制）时，形式化方法可以利用这些信息并缩小可达集，提供车辆运动“更紧”的预测，形成在线安全监控和验证等有价值的应用。相反，如果控制策略是专有的且完全未知（黑盒控制），则安全验证过程必须涉及每次模拟仿真后黑盒控制器行为的统计学习，这反过来将指导选择下一个要测试的场景，以更好地针对反例。
A.白盒已知控制政策的形式化安全验证。如果完全了解控制策略（通常仅限于自车），则可以非常确定地执行安全验证，有效地消除可达性分析（RA）中的控制变量u。这通常是，计算受控车辆的可达集并将其与相关时间间隔内的障碍物占用集进行比较，来实现的。
B.黑盒控制政策的形式化安全验证。当控制策略完全未知时，验证需要退回到不需要控制策略信息的更一般的计划。此类计划将控制器和平台视为一个整体系统，并调查整个系统的输入（如干扰）如何导致不期望的输出（如安全违规）。一项关于黑盒验证的综述论文列出模拟退火、进化算法、贝叶斯优化或扩展蚁群优化（ant colony optimization）等几种方法。
C.灰盒控制政策的形式化安全验证。如果控制策略部分已知，则可以执行修改的可达性分析（RA）形式化方法。在半自动车辆的设置中，人类驾驶员的行为最多只能进行估计，必须用部分已知的控制策略（本例即人类驾驶员策略）进行安全验证。在此设置中，设计的特定车道保持辅助控制器将人类驾驶员的转向策略视为已知且不可变，而将人类驾驶员的加速策略视为未知且可变。这种处理方法允许可达性分析（RA）在适当的时间范围内预测车辆的可达状态范围，系统可以通过比较当前车辆状态和后向可达安全集（BRS）来确定人类驾驶员是否需要帮助。当至少知道控制策略或功能的定性目标时（例如，激活干预，避免车辆因驾驶员误操作而发生可避免的碰撞），则可以使用可达性分析（RA）来验证此类控制策略或功能是否忠实于其定性描述。例如，用于判断防撞系统是否错过或滥用了干预机会。
如下表是：部署的形式化和提供的保证类型
形式化（formal）方法可以提供有关当前驾驶状况紧要性的有用信息。该信息可用于制定标准，以确定是否需要不同的控制方案，从安全紧要场景中把自车带入安全。
其中一个仲裁标准是车辆是否处于不可避免碰撞状态（inevitable collision state，ICS），有人认为，在估计碰撞频率时，这是一个比传统的威胁度量，如，更可靠的碰撞接近度量，是ISO26262中确定汽车安全完整性水平（automotive safety integritity level，ASIL）的关键量。如果车辆确实处于这种状态，则应进行碰撞准备（通常通过制动减速或遵循非故障轨迹），因为碰撞是不可避免的。该概念已被用于ADAS功能原型，如确定何时触发自动紧急制动（AEB）或执行避碰动作。为了确定此类ICS，通常使用可达性分析（RA）。当移动障碍物的预测在动态交通场景中至关重要时，创建ICS概率等价的概率框架。对于某些半自动驾驶或ADAS功能，确定系统是否处于不可避免碰撞状态（ICS）有助于确定ADAS干预是否遗漏或不必要。
另一个仲裁标准是，在系统当前的运动模式下，目标状态是否可以实现。例如，用修剪轨迹的概念对车辆的运动模式进行分类，其特征是保持运动所需的恒定输入。可以建立某个系统的轨迹库，供控制器从中选择。在这种情况下，持续的可行性（continuous feasibility）和控制活力（control liveliness）是确保完成更高级任务的关键因素，如超车、并入繁忙的快车道或避开高速的障碍物。如果从大型复杂动态模式库中选择模式需要计算，可以利用基于学习的方法（如强化学习），根据环境有效地学习适当的模式仲裁决策。
可达性也可以“随时”直接集成到控制系统中，为现任控制器提供持续的指导/倾向性，避免不可能的控制造成的灾难性事件。
这种直接控制集成方法之一是模型预测控制（MPC），其中可以使用形式化方法，尤其是可达性分析（RA）来开发鲁棒的MPC算法，如图所示：可达性分析用于为每个MPC规划范围找到可行的状态集，这样生成的MPC算法不会试图在不可行区域中找到最优解，因为那些区域会导致不稳定或控制失败。
这也被称为递归可行性或持久可行性。当可达集约束为概率时，可以开发鲁棒MPC随机等价的模型。除了鲁棒性和可行性保证之外，RA应用于MPC的其他好处，包括建立系统输入到状态稳定性的潜在方法，将基于学习MPC的鲁棒性和性能分离，移除永远无法到达的区域来显式降低MPC的复杂性。
将形式安全性集成到控制设计中的另一种方法是生成安全参考轨迹，如图所示：可达性可用于轨迹规划阶段，生成最安全且物理上可行的轨迹，供较低层的控制器遵循。
最后是安全的开放性问题和资源。
1 开放性问题
1） 保真度-速度权衡
2） 数据驱动的可达性方法
3） 超越二进制安全验证
4） 构建安全描述的新逻辑
5） 具有可达性的道德验证
2 资源问题
1） 可达性分析的数值方法
如下表所示的清单：
2） 可达性分析的软件工具
如下表给出的清单：
本文仅做学术分享，如有侵权，请联系删文。
1.面向自动驾驶领域的多传感器数据融合技术
2.面向自动驾驶领域的3D点云目标检测全栈学习路线！(单模态+多模态/数据+代码)3.彻底搞透视觉三维重建：原理剖析、代码讲解、及优化改进4.国内首个面向工业级实战的点云处理课程5.激光-视觉-IMU-GPS融合SLAM算法梳理和代码讲解6.彻底搞懂视觉-惯性SLAM：基于VINS-Fusion正式开课啦7.彻底搞懂基于LOAM框架的3D激光SLAM: 源码剖析到算法优化8.彻底剖析室内、室外激光SLAM关键算法原理、代码和实战(cartographer+LOAM +LIO-SAM)
9.从零搭建一套结构光3D重建系统[理论+源码+实践]
10.单目深度估计方法：算法梳理与代码实现
11.自动驾驶中的深度学习模型部署实战
12.相机模型与标定(单目+双目+鱼眼）
13.重磅！四旋翼飞行器：算法与实战
14.ROS2从入门到精通：理论与实战
扫码添加小助手微信，可
也可申请加入我们的细分方向交流群，目前主要有、、、、、等微信群。
一定要备注：，例如：”3D视觉 + 上海交大 + 静静“。请按照格式备注，可快速被通过且邀请进群。也请联系。
▲长按加微信群或投稿
▲长按关注公众号
：针对3D视觉领域的五个方面进行深耕，更有各类大厂的算法工程人员进行技术指导。与此同时，星球将联合知名企业发布3D视觉相关算法开发岗位以及项目对接信息，打造成集技术与就业为一体的铁杆粉丝聚集区，近4000星球成员为创造更好的AI世界共同进步，知识星球入口：
学习3D视觉核心技术，扫描查看介绍，3天内无条件退款
圈里有高质量教程资料、答疑解惑、助你高效解决问题