arXiv于2022年2月6日上传了综述论文《AutomatedVehicleSafetyGuarantee,VerificationandCertification:ASurvey》，作者来自俄亥俄州立大学。与自动驾驶相关的挑战不再仅仅集中于自动驾驶汽车(AV)的制造，而是确保其安全运行。3级和4级自动驾驶的最新进展促使对复杂AV操作的安全保证进行更广泛的研究，这与ISO21448（预期功能安全或SOTIF）的目标一致，以最大限度地减少已知和未知的不安全场景，以及“零”Fatality(VZ)'——到2050年消除道路死亡事故。大多数为AV运动控制提供安全保障的方法都源于形式化方法，尤其是可达性分析（RA），它依赖于系统动态演化的数学模型来提供保障。本文概述了安全验证与验证和认证过程，并回顾了最适合AV的正式安全技术。作者提出了一个统一的场景覆盖框架，可以为全自动驾驶汽车提供形式化或基于样本的安全验证评估。最后，AV安全保障面临挑战和未来机遇。以前对自动驾驶汽车技术的评论主要集中在技术挑战和实施方面，例如感知、决策、车辆控制、人机交互的执行方式，一些调查已经解决了自动驾驶汽车安全验证和确认(V&V)问题.随着自动驾驶系统在现实世界中的部署，需要针对现实场景的规模进行大量的验证和验证。最大化场景覆盖率的常见验证和验证策略是在虚拟仿真中进行验证并模拟大量生成的场景样本。基于场景采样的V&V面临的挑战是量化确保合理覆盖所需的样本量，从而约束自动驾驶不当驾驶带来的风险。合理的场景覆盖保证也是最近在高度自动化车辆(HAV)部署立法中获得认证的先决条件。然而，另一组基于形式验证的方法通过规范满足以不同的方式解决了场景覆盖问题。由于场景覆盖形式化方法的潜力，新兴研究开始将形式化属性与控制综合和安全验证相结合。针对自动驾驶量化验证的需求，本文提出了统一的场景覆盖框架，以解决自动驾驶场景覆盖中尚未解决的难点问题。给定单个场景可接受覆盖率的表示（基于样本的方法），或所谓的正式安全规范的“规范渗透率”，该框架给出了统一安全场景覆盖率的量化定义。这种量化定义结合了基于样本和形式化的方法，为安全验证提供了场景覆盖。候选的自动驾驶车辆控制策略可以通过形式化或基于样本的安全验证来测试其在指定ODD（操作定义域）场景中的安全场景覆盖率。作者比较了基于样本的方法和正式方法的优缺点，基于如何实现这种安全覆盖，以及相关的成本和对这些方法的争论。下表展示了自动驾驶立法的现状：责任认定是自动驾驶系统部署需要解决的新问题。在L3级别，只要提前将突发情况或困难情况交给驾驶员，自动驾驶系统就无需负责，因为它只需要在其有限的ODD环境中保持安全即可。即使人类驾驶员没有及时接管，刹车、停车、开启危险灯等故障安全动作也能在一定程度上减轻自动驾驶系统的负担。L4级及以上自动驾驶汽车在进行形式化安全验证时，可以根据形式化逻辑简化责任认定，如下图：Aautomaticdrivingsystemdevelopedbasedonsamplesafetyverification,itisnotclear如何以责任确定的形式执行类似的程序。广泛使用的安全指导标准，ISO26262Roadvehicles-Functionalsafety，仅适用于减轻与已知组件故障相关的已知不合理风险（即已知的不安全条件），但并未解决自动驾驶因复杂环境变量而导致的驾驶风险，以及自动驾驶系统如何应对这些风险，而不让汽车出现任何技术故障。鉴于上述安全挑战，ISO21448提出了一个定性目标，描述目标（goals）以最小化自动驾驶功能设计的已知和未知的不安全场景结果，如图：然而，要实现这个SOTIF目标挑战在于，传统的方法，例如现场操作测试，无法覆盖测试过程中自动驾驶的所有可能场景。尽管存在挑战，但安全分析中仍有一些有前途的方法和方向可以朝着ISO21448的目标迈进，例如最大化模拟测试中的场景覆盖，或创建ASD。在技??术术语中，“足够安全”通常是指对指定的ODD场景进行完整或充分的场景覆盖。事实上，现有法规的要求相对较弱，仅要求检查“少数关键场景”。在离散场景周围引入“增量邻域”，将“数量”分配给场景样本，这是一种很有前途的尝试。T-wise和泊松过程等数学算法可以通过巧妙地选择有限样本的候选者来实现“几乎完全”的统计覆盖。乐观地假设这个量化的覆盖表示问题得到解决并被整个社区接受，每个采样场景都有一个“覆盖量”。基于样本方法的全场景覆盖任务将执行足够数量的样本验证测试，以确保每个“覆盖”单元与至少一个安全测试结果相关联。事实上，有些场景空间的存在，恐怕无法产生安全测试结果（例如对障碍物的反应距离太小）。在这种情况下，需要额外的努力来确认这些场景确实不安全。在型式批准和认证方面，当权者需要设定一个可接受的成功门槛，以满足公众的期望。最简单的阈值是确认安全性的不同测试数量与ODD场景测试所需的最少测试数量之比。多样化的测试场景采样是自动驾驶研发阶段加强安全管控的主要方式之一。在实现最小化已知和未知不安全场景的SOTIF优化目标方面，基于样本的方法在发现未知不安全场景方面具有更小的偏差和更强的探索力，从未知到已知的推动是“级别一致性”，即所有采样场景通常处于一致的模拟环境中，并且具有相同的保真度。图中展示了形式化方法和基于样本的方法的场景覆盖率对比：形式化方法从更抽象层的安全规范出发，在场景空间中可能有更大的单一覆盖率，但是整合了形式化规范控制合成或监控的过程可能依赖于控制器数学并且很麻烦；由于随机生成过程，基于样本的方法具有更分散的场景覆盖，但直接从模拟层开始覆盖案例，这使得采样过程简单易行。这两种方法都试图将最大的验证场景投射到真实驾驶中，但模拟层与真实驾驶之间的差异始终存在。与基于测试的安全验证和保证方法相比，形式化方法具有严格的逻辑基础，因此具有较高的语句可靠性。自动驾驶汽车安全性中常用的形式化方法包括模型检查、可达性分析和定理证明。模型检查起源于软件开发，以确保软件根据设计规范运行。当安全规范用公理和引理表示时，定理证明可用于验证最坏情况假设下的安全性。可访问性分析在这三种分析中占有特殊的地位，因为它具有为动态系统生成安全声明的固有能力，捕捉动态驾驶任务(DDT)的主要特征。真实世界的道路测试或现场操作测试(FOT)是自动驾驶汽车验证和验证(V&V)的最终且昂贵的方法。从某种意义上说，这是验证的唯一方法。但是，FOT的缺点也很明显：缺乏足够的场景覆盖（尤其是接近碰撞和已经碰撞的场景），并且在车辆上安装了候选自动驾驶控制器。该图显示了基于样本、正式和现场操作测试(FOT)方法的比较：分数范围从0到10，其中10代表最高满意度。形式化方法是一类应用数学中严格的技术（通常以逻辑计算的形式）来实现软件和工程设计规范和验证的方法。顾名思义，其在安全验证任务中具有先天优势，但系统复杂度高、动态连续性一直是其在自动驾驶领域广泛应用的主要限制因素，即可扩展性带来的困难。从技术上讲，形式化方法可以概括为将抽象规范实现或转化为系统控制算法/程序，使受控系统行为满足描述规范的过程。定义动态系统：最大前向可达集（MaximalForwardReachableSet）定义如下：前向可达集（FRS）传播动力学，从初始时刻t0到未来时刻t所有可能的可达状态。相比之下，向后可达集（BRS）的向后传播寻找从前一个时间t到当前时间t0到达某个目标状态集Xgoal的所有可能状态，即下面的最大向后可达集（MaximalBackwardReachableSet）此外，最小BRS定义为：在某些情况下，定义时间范围内的可达性更有趣。因此，将定义扩展到包括从当前时间到时间范围的末尾，例如，修改了最大前向可达集的定义（其他类比）：当不同流量参与者之间的交互起关键作用时，参与有时必须是可访问性分析中甚至包括拮抗剂的影响。在这种情况下，动力系统引入了一个额外的输入d来表示这种对抗性控制输入：这样，系统中对抗性输入的影响不依赖于自我车辆控制，因此必须保守地建模，以便在最坏情况下提供安全保障。以下是进一步限制对抗性影响下的最大FRS的定义：在计算机科学和机器人领域，信号时间逻辑(STL)是一种通用语言，用于表达和指定涉及连续变量的时间关键要求。下表列出了STL的基本语义。简而言之，STL使用一阶逻辑（定义为一组对非逻辑对象（例如变量）进行量化的形式系统）来解释变量的时域发展。下表是基本的STL语义：自动驾驶车辆的临时安全规范示例可能是“永远不会在交通中造成碰撞”，但是一旦转换为STL规范，临时规范中的一些歧义就需要解决。首先，STL中对“原因”一词的定义不明确，因为它涉及确定碰撞责任的复杂性，可能必须用“在”一词代替，这是一个责任中立的陈述。临时规范随后变成“永远不要在交通中发生碰撞”。其次，STL要求规范具有精确定义的时间范围。对于自动驾驶，时间框架的概念通常用于将时间跨度缩小到实用和可管理的水平。因此，临时规范可以进一步修改为“从不（在时间范围内）发生碰撞”。上述STL翻译的安全规范在既定语言中仍停留在抽象层面，自动驾驶车辆控制算法设计者有责任将规范综合到控制器架构中，或对设计的控制器进行安全验证，有足够的信心或确定性。证据确保它符合规范。除了控制综合之外，STL中表达的安全规范还可以在控制器原型制作期间用作断言以指示安全违规，因此开发人员在控制设计期间不断了解安全规范。确定安全规范的逻辑计算通常是通过求解一个决策满足模数理论（SMT）问题来完成的。基于采样的方法通过填充大量场景样本来验证场景变化。与基于采样的方法不同，形式验证侧重于在环境模拟中以一定程度的保真度在控制器中实施安全规范。这是由于验证安全性的不同机制。在形式化的安全哲学中，要么满足安全规范，要么违反安全规范，规范的满足被综合到基于模型的控制设计中。设计完成后，运行中保证执行的责任转移到模型正确性的在线验证上：只要验证面向控制的模型正确，控制器按照综合安全规范执行，系统可以证明是安全的。在不失一般性的情况下，安全规范φ在某些情况下（例如不可避免的碰撞）可能不可行，?u,(s,t)/|=φ。在这种情况下，φ-合成控制器无法找到可行的控制序列来实现φ，最好的行动方案是将情况升级为有预谋的紧急情况或应急策略（如碰撞冲击准备）。在任何情况下，由于设计的φ-合成控制器已用尽其可用动作并且仍然无法找到φ-令人满意的动作，因此控制器不会因不可避免的损坏而被视为故障。根据ISO21448，场景是一系列场景中几个场景之间时间发展的描述，场景是环境的快照，包括场景、动态元素、所有参与者和观察者。表示，以及这些实体之间的关系。根据这个定义，在定义的OOD中确保完全安全的任务可以描述为对ODD所有可能的场景变化进行安全验证和确认（V&V）。ODD中的场景变化有两个方面：初始场景的变化，以及从初始场景开始时间发展的变化。场景变化的不同维度如图所示：基于样本的方法没有明确地具有与每个样本场景关联的体积属性，因为每个场景样本都是基本的并且具有较小的体积。为了统一比较和利用两种安全验证方法，必须将场景体积的概念赋予基于样本的方法。为简单起见，假设所有N个连续维度相互正交，并为参数集指定的场景样本分配一个N维场景空间的轴对齐多边形体积“p01，p02，...，p0N”.在基于样本的方法中，在每个场景样本中检查模拟场景的安全性。另一方面，形式化方法通常在执行任何模拟之前从安全规范开始，然后将规范转换为机器可理解的语言语句，例如线性时域逻辑(LTL)或信号时域逻辑(STL)。然后通过在模拟/真实世界测试中检查规范的有效性，或者通过在控制综合期间将规范转换为系统约束或其他控制设计功能来应用翻译后的规范。理想情况下，对于形式化方法，如果所有与安全相关的规范首先被真实地翻译成此类机器可理解的陈述，并且如果合成控制器完全遵守这些陈述并使用基于模型的控制器对（模拟）环境进行完美建模，那么场景覆盖相对于模拟层为100%。例如，“自动驾驶车辆应始终无碰撞”这一表达可以转化为数学函数形式的可验证表达式，评估自动驾驶车辆与模拟中任何其他目标之间的占用重叠模型，如果重叠发生在仿真中，则返回真。然而，实际挑战阻碍了正式安全规范的100%理想翻译，原因如下：首先，正式方法依赖于基于现实世界抽象的视图，因此抽象与现实之间会出现差异（无论大小），以及妥协有效的安全保障。其次，实际开发的控制器通常存在性能限制，无论如何都不符合安全规范。第三，在形式化安全规范以转化为安全验证或控制综合时存在实际的可扩展性困难。也就是说，形式化方法在现实中的普及率通常不到100%。形式上，渗透率定义为：正式安全规范规定的场景子空间中可验证场景的百分比。在实践中，找出给定ODD中自动驾驶车辆候选控制器的规范渗透可能是一个挑战。首先，定理证明等演绎形式方法仅限于相对简单的离散动力系统，将定理证明扩展到连续动力系统需要进一步建立框架和大量计算资源。其次，传统的算法形式化方法，如模型检查，不适用于连续动态系统。当需要对连续的动作空间进行精细离散化时，对所有可能的动作进行详尽的测试也会导致计算资源问题。.然而，最近将STL与可达性分析相结合的进展可以通过计算ODD场景空间中候选控制器的验证算法来评估这种渗透率，并预测不符合STL规范的候选控制器的数量。体积部分。典型渗透率计算问题仍然是一个悬而未决的问题，未来的工作可能会结合不同的证据收集方法，包括演绎和算法，以提供不同的替代方案。完成场景覆盖的路线如图所示：形式化方法和基于样本的方法都是帮助发现自动驾驶汽车安全控制薄弱环节的有效工具，自动驾驶汽车控制开发者可以任选其一他们根据自己的方便和喜好。一种或两种方法。这张图其实是安全验证的控制策略演化示意图。在(a)-(e)中，形式化方法从ODD(a)的安全规范开始，然后进行初始安全规范渗透测试，以查看安全规范维护得如何(b)。然后执行可行性检查以查看有多少失败的场景实际上是安全可行的(c)。然后重新设计自主车辆的控制器以修复故障场景体积区域（d），最后用候选自主车辆控制器验证所有安全可行的场景体积的安全性。在(f)–(j)中，基于样本的方法首先将ODD分割成可验证的场景单元(f)，然后执行不完整的采样安全测试以检查候选AV控制器(g)的主要问题。随后进行全饱和采样以确保场景覆盖(h)。全场景覆盖测试后，控制器的弱点暴露出来，重新设计的过程将重复（i）。最终，控制器的弱点停止减少，控制器重新设计过程可能结束（j）。请注意，使用正式方法，可以识别安全不可行场景区域，并且一旦验证了ODD中除安全不可行场景体积之外的所有体积，就不需要进一步重新设计。安全验证可以在模拟（在线）期间使用预测模块进行，也可以在模拟（离线）之后，简单地检查结果，如图所示，不同验证方案的概述：当自我车辆和参与交通代理当控制策略已知（白盒控制）或部分已知（灰色控制）时，形式化方法可以利用这些信息缩小可达集，提供“更严密”的车辆运动预测，形成在线安全监控的有效模型和验证等应用价值。相反，如果控制策略是专有的且完全未知（黑盒控制），则安全验证过程必须涉及在每次模拟仿真后对黑盒控制器行为的统计学习，这反过来将指导选择下一个要测试的场景，更好的针对反例。A.已知控制策略的正式安全验证。如果控制策略完全已知（通常仅限于自我车辆），则可以高度确定地执行安全验证，从而有效地从可达性分析??(RA)中消除控制变量u。这通常是通过计算受控车辆的可达集并将其与相关时间间隔内的障碍物占用集进行比较来实现的。B.黑盒控制策略的正式安全验证。当控制策略完全未知时，验证需要回退到不需要控制策略信息的更通用的计划。此类程序将控制器和平台视为一个整体系统，并研究整个系统的输入（例如干扰）如何导致不希望的输出（例如安全违规）。一篇关于黑盒验证的评论文章列出了模拟退火、进化算法、贝叶斯优化或扩展蚁群优化等等。C.灰盒控制策略的形式化安全验证。如果控制策略部分已知，则可以执行修改后的可达性分析??(RA)形式化方法。在半自动车辆的设置中，人类驾驶员的行为最多只能被估计，并且必须使用部分已知的控制策略（在本例中为人类驾驶员策略）进行安全验证。在此设置中，设计的特定车道保持辅助控制器将人类驾驶员的转向策略视为已知且不变的，并将人类驾驶员的加速策略视为未知且可变的。这种处理方法允许可达性分析（RA）预测车辆在适当时间范围内的可达状态范围，系统可以判断人类驾驶员是否需要帮助。当至少已知控制策略或功能的定性目标时（例如，激活干预，避免由于驾驶员错误导致的车辆碰撞），则可以使用可达性分析来验证此类控制策略或功能（RA)是否忠实于其定性描述。例如，确定防撞系统是否错过或滥用了干预机会。下表是：可访问性分析(RA)部署的形式化和提供的保证类型形式化方法可以提供有关当前驾驶条件的关键性的有用信息。此信息可用于制定标准，以确定是否需要不同的控制方案来使自我车辆从安全关键场景中恢复安全。仲裁标准之一是车辆是否处于不可避免的碰撞状态（ICS），在估计碰撞频率时，这被认为是比传统威胁指标（例如碰撞时间（TTC））更可靠的碰撞方法。ISO26262中的关键数量，以确定汽车安全完整性等级(ASIL)。如果车辆确实处于这种状态，则应该为碰撞做好准备（通常通过制动减速或遵循非故障轨迹），因为碰撞是不可避免的。该概念已用于ADAS功能的原型设计，例如确定何时触发自动紧急制动(AEB)或执行防撞操作。为了识别此类ICS，通常使用可达性分析??(RA)。当移动障碍物的预测在动态交通场景中至关重要时，为ICS的概率等价创建了一个概率框架。对于某些半自动驾驶或ADAS功能，确定系统是否处于可避免的碰撞状态(ICS)可以帮助确定ADAS干预是否被遗漏或不必要。另一个仲裁标准是目标状态是否可以通过系统的当前运动模式实现。例如，修剪轨迹的概念用于对车辆的运动模式进行分类，其特征是保持运动所需的恒定输入。可以建立一个系统轨迹库，供控制器选择。在这种情况下，连续可行性和控制活泼性是确保完成更高级任务的关键因素，例如超车、并入繁忙的快速车道或高速避障。如果从大型复杂动态模式库中选择模式需要计算，则可以利用基于学习的方法（例如强化学习）来根据环境有效地学习适当的模式仲裁决策。可达性也可以直接集成到“移动中”的控制系统中，为现任控制器提供持续的指导/倾向，避免因无法控制而导致的灾难性事件。这种直接控制集成方法之一是模型预测控制（MPC），其中形式化方法，尤其是可达性分析（RA）可以用来开发鲁棒的MPC算法，如图：ReachabilityanalysiswithThegoalistofind每个MPC规划范围的可行状态集，以便生成的MPC算法不会尝试在不可行区域中找到最优解，因为这些区域会导致不稳定或控制失败。这也称为递归可行性或持续可行性。当可达集约束是概率性的时，可以开发随机等效于鲁棒MPC的模型。除了鲁棒性和可行性保证之外，将RA应用于MPC的其他好处包括建立系统输入到状态稳定性的潜在方法，将鲁棒性和性能与基于学习的MPC分离，以及删除永远无法到达的区域以明确降低复杂性MPC。将形式安全集成到控制设计中的另一种方法是生成安全参考轨迹，如图所示：可在轨迹规划阶段使用可达性来为下级控制设备生成最安全和物理上可行的轨迹。最后，安全1的开放问题和资源开放问题1）保真度-速度权衡2）数据驱动的可达性方法3）超越二进制安全验证4）构建安全描述的新逻辑5）可达性2道德验证的资源问题1)可达性分析的数值方法列表如下表：2)可达性分析的软件工具列表如下表：
