经过形式化验证的自动驾驶故障运行安全概念

标签：CSM AD 故障 验证 形式化 安全 DSM VSM

经过形式化验证的自动驾驶故障运行安全概念

**摘要：**现代自动驾驶(AD)系统依靠安全措施来处理故障并使车辆处于安全状态。为了消除致命的道路交通事故，汽车制造商不断推出新的感知和控制系统。当代汽车设计和安全工程最佳实践适用于单独分析系统组件，而当今高度复杂且相互依赖的AD系统需要新颖的方法来确保对多点失效的恢复能力。我们提出了一个整体安全概念，统一了处理多点失效的先进安全措施。我们提出的方法使设计人员能够专注于更紧迫的问题，例如处理与系统性能限制相关的无故障危害行为。为了验证我们的方法，我们在形式化规范语言mCRL2中开发了一个安全概念的可执行模型。模型行为由控制分布式处理器、冗余通信网络和虚拟机的四模式降级策略控制。为了尽可能保证车辆的安全，我们的降级策略可以使用额外的低成本驾驶通道来降低驾驶舒适度AD系统的可用性。我们在模态µ演算中形式化了五项安全要求，并根据我们的mCRL2模型对其进行了证明，而使用传统道路测试或模拟技术很难彻底实现这一点。总之，我们经过形式验证的安全概念为设计AD系统定义了一种整体设计模式。

附赠自动驾驶最全的学习资料和量产经验：链接

01.简介

自动驾驶汽车乘客和其他道路使用者的安全取决于自动驾驶(AD)系统。为了提高交通安全，政府和汽车行业制定了“零事故愿景”，目标是在未来彻底消除道路交通事故死亡。要设计AD系统，汽车安全工程需要可靠的产品生命周期管理、安全分析技术和设计模式。最先进的安全标准和指南（ISO 26262、ISO/PAS 21448 SOTIF、SaFAD、RSS、IEEE P2846等）旨在降低因系统故障、无故障危害行为和错误驾驶决策而导致的风险。我们工作的贡献是：通过提供整体的故障运行设计模式和探索将形式化验证应用于新型高弹性降级策略的有前景的实践。

ISO 26262标准侧重于由于随机硬件故障和系统软件故障导致的系统故障。根据该标准，汽车安全完整性等级(ASIL)表示AD元素所需的完整性。具有较高ASIL的元素需要更可靠，但开发成本也更高。商业上可行的AD系统倾向于具有较少高ASIL元素的经济高效的解决方案。ASIL分解过程可以帮助降低所需的ASIL，前提是具有足够的架构、硬件或软件独立性。

传统的汽车系统只需要故障安全机制，但是，AD应用（尤其是自动化等级3+）需要故障运行能力。开发故障运行AD系统需要复杂的安全分析，例如相关失效分析和确保对多点故障具有弹性。在本文中，我们分析了如何处理双点和一些三点故障。我们提出的解决方案提供了故障运行能力，同时限制了高ASIL元素的数量以优化成本。

此外，AD应用程序需要在没有故障的情况下进行态势感知，以监控其自身的性能限制，如SOTIF中所述。针对性能限制的常见安全措施是遵循取决于操作设计域(ODD)的降级策略。ODD指定AD应用程序设计为正确控制车辆的条件，例如道路类型、速度范围、天气和光照条件。请注意，AD组件在不同的ODD（例如基于机器学习的组件）中可能具有不同的性能，并且可能并不总是安全的。

ISO 26262并不严格要求形式验证技术，而是侧重于传统方法，例如失效分析技术、测试和验证。不幸的是，传统技术并不详尽且不省时，导致在开发或现场安全问题识别较晚。相比之下，形式模型检查通过详尽证明安全属性来减少代价高昂的规范错误。值得注意的是，IEEE P2846工业工作组目前正在使用车辆运动学的数学公式定义自动决策的形式模型。

我们提出了一种基于分布式安全机制(DSM)的安全概念，用于自动驾驶，具有能够处理多点故障的各种降级模式。为了验证我们的方法，我们使用形式化规范语言mCRL2对DSM行为进行建模。DSM模型的安全要求经过定义、形式化和形式化验证。

本文做出了以下贡献：

1. 基于DSM的故障运行安全概念（包括行为规范），使用降级模式处理多点故障和性能限制，并将故障模型和监控技术分配给DSM的不同安全层。

2. 使用mCRL2语言对DSM模型进行形式化规范，并形式化验证DSM降级模式的安全要求。

本文的其余部分组织如下。在第2节中，我们概述了相关工作。然后，我们在第3节描述了DSM架构。我们在第4节讨论了故障模型和监控技术在DSM安全层的分配。我们在第5节详细阐述了故障处理和降级模式行为。第6节介绍了DSM模型和形式验证过程。最后，我们在第7节得出结论。

02.相关工作

在本节中，我们将概述与我们的工作最相关的相关AD系统的安全架构以及形式化建模在汽车领域的应用。

2.1 自动驾驶的安全架构

有研究提出了一种使用虚拟机管理程序和不同中间件软件堆栈的分布式安全机制。该安全机制是在带有自动驾驶模拟器的硬件在环设置上实现的。还提出的DSM通过硬件在环模拟的概念验证实验进行评估，以便能够检测AD系统中的单点故障并在必要时安全停止车辆。我们的工作继承了研究中的分层架构以及软件中间件和虚拟机管理程序的使用。然而，与专注于DSM架构的概念验证实现的研究相比，我们的工作改进了安全概念以启用更多降级模式。此外，我们对DSM故障处理行为的逻辑进行了建模和形式验证。

（参考文献1，添加（猿东东微信：AlphaApe）免费领取）提出了一种可扩展的AD系统架构。在这种架构中，有一个主ASIL通道，可为乘客提供先进的自动驾驶功能和舒适度。在同一平台上，还有第二个ASIL通道，其功能不太先进。但它具有更安全的轨迹规划，因此比主通道更安全。实现了选择器以在两个ASIL通道之间切换。此外，在单独的平台上实现了故障降级通道，可以访问冗余制动和转向。可扩展性和集成性是此设计的主要重点。与依赖冗余执行器进行降级运行的（参考文献1）相比，我们的DSM依赖冗余通信网络、中间件堆栈、虚拟机管理程序和不同的监控技术来实现各种降级形式的AD系统操作。

有研究提出了一种故障运行架构，该架构在出现故障时仍可运行。它有两个双通道域控制器。四个通道中的每一个都由一系列传感器系统、基于AI的数据处理和控制以及执行器系统组成。请注意，只有数据处理和控制系统对于每个通道是独立的，所有其他子系统都在通道之间共享。从这个意义上说，我们的DSM中的辅助通道更加孤立，因为它具有不同的AD系统功能实现，其数据来自专用的安全传感器。在另外的研究中，每个通道都有多个监视器，它们都向同一通道中的全局安全/故障管理器报告。该集中式通道安全管理器负责通道中的故障遏制和响应功能。类似的系统是在百度阿波罗AD框架中实现的集中式健康监视器，以及研究中描述的集中式AD系统模式管理器。相反，我们的DSM支持所有安全层中的分布式监视器。故障检测不是报告给集中式监视器，而是报告给中间件软件提供的诊断消息主题。研究提出的另一个有趣的观点是，找到最小风险安全停止所需的时间是不确定的，可能需要几分钟。我们的DSM通过在AD系统的某些降级模式下提供进一步的降级来应对这一挑战。还有研究讨论了几种应用安全执行模式的卡车队列架构的系统级安全系统。所描述的架构实现了两个在不同平台上运行的异构通道。使用不同的投票机制在两个通道之间进行仲裁。如果其中一个通道发生单一失效，这种异构双工模式可以故障运行。在DSM中，我们还在正常通道旁实现了一个异构安全通道，并将故障处理扩展到多点故障。

（参考文献2，添加（猿东东微信：AlphaApe）免费领取）描述了一种用于自动驾驶汽车的监视器/执行器架构，也称为执行者/检查者架构。该架构依赖于理想的监视器来检测主系统中的失效。然后，简单且高完整性的失效转移系统可以将车辆置于安全状态。

我们的DSM启用的多种降级运行模式类似于（参考文献3，添加（猿东东微信：AlphaApe）免费领取）中描述的故障转移任务。DSM的优势在于，通过利用分层架构和不同的监控技术，即使监视器出现故障，我们仍然可以保证故障运行。

（参考文献4，添加（猿东东微信：AlphaApe）免费领取）提出了一种用于AD系统的功能通用架构。有一个或多个AD系统模式管理器模块，它们根据从多个监视器收到的信息将AD系统从正常操作切换到降级操作。虽然在相当高的层次上描述了它的框架，但我们为我们的DSM提供了足够的低级硬件细节和高级安全机制行为，并将故障模型和缓解技术分配给了DSM架构。

2.2 自动驾驶的建模和形式化方法

责任敏感安全(RSS)和相关IEEE P2846工作组定义了一个安全驾驶决策的数学模型。该模型强制执行车辆之间的纵向和横向距离、通行权和规避动作。它从法律角度定义了一种“安全状态”，旨在防止自动驾驶汽车成为交通事故的根源。请注意，RSS假设AD系统永远不会发生故障并且没有性能限制，例如，感知子系统可以完美地检测所有道路使用者。此外，RSS模型是技术中立的，忽略了片上系统、网络和软件中的安全关键影响。我们的安全概念将RSS作为驾驶决策的关键组成部分。为了解决RSS限制，我们的概念使用了其他技术；例如，系统监控和反应机制来解决AD系统故障。

有研究使用SysML图给出了线控刹车系统的简化故障操作模型，并使用活动图分析了转换。如果正常通道发生失效，则有仲裁逻辑来激活后备通道。假设一个通道中的故障与另一个通道中的故障无关。有一种紧急操作模式和一种驾驶员接管模式以防发生失效。研究中的两个通道都是故障静默的，这意味着它们在发生失效时将保持静默状态并且不会产生任何输出，而不会干扰任何组件，从而防止失效在组件级别传播。我们的安全概念假设只有一个安全层是故障静默的，并依靠虚拟机(VM)来防止故障传播。此外，在DSM中实现了更多降级模式来处理多点故障。

研究还使用故障树分析(FTA)基于状态机和系统活动图推导出故障树失效模型。结果是符合ISO 26262的安全框架。虽然研究中没有采用任何形式化方法，但强调了证明仲裁逻辑和系统无死锁属性正确性的必要性，并提出了形式化验证作为防止控制故障运行驱动的状态机逻辑失效的解决方案。

还有研究提出了一个框架来捕捉AD系统设计与功能安全之间的关系。该研究讨论了形式化验证在汽车领域的优势和好处，并建议应用形式化方法来帮助解决ISO 26262或SOTIF未涵盖的非预期功能和突发行为的问题。

03.安全机制的架构

在以下小节中，我们将详细介绍我们安全概念中的DSM架构和组件功能。

3.1 分布式安全机制的功能

图1说明了我们DSM的高级架构。请注意，我们不会将架构限制在任何特定实现上，而只是出于说明目的给出实现示例。下面描述了每个组件的功能。

图1：具有分布式安全机制的自动驾驶系统架构

a) AD和ODD传感器：AD系统中有AD传感器和ODD传感器。AD传感器通过主网络向功能(FUN)层上的特定AD功能模块提供数据。例如，摄像头和雷达传感器向感知功能模块提供数据，而全球导航卫星系统则向定位模块提供数据。同时，传感器和功能监控(SFM)层监控AD传感器数据。ODD传感器的目的是通过主网络向集成在SFM层中的ODD检查器提供输入。

b) 安全传感器：有热备用传感器通过辅助网络产生用于安全操纵的数据，这些数据由车辆安全机制(VSM)层接收和监控。

c) 功能(FUN)层：在FUN层中，AD功能模块（例如定位、感知、路径规划等）正在运行。FUN层只能访问主网络通道。一个或多个具有相关功能的模块在同一个VM中运行。请注意，安全相关的决策算法（例如RSS）通常集成在路径规划模块中，百度阿波罗AD平台就是这种情况。

d) 中间件：中间件是一种使分布式系统的各个组件能够可靠通信和管理数据的软件。通信的可靠性和可见性由中间件服务质量(QoS)策略保证，例如实时截止时间、优先级和可靠性。请注意，中间件通信协议必须没有单点失效，例如，参见数据分发服务(DDS)标准。在我们的DSM中，我们假设信息在使用发布-订阅通信模式的可靠中间件之上共享。

e) 传感器和功能监视器(SFM)层：每个VM都有一个SFM层。SFM监视同一VM中FUN层的状态。此外，它还检测相应AD传感器输入和输出中的故障，例如时序抖动和超出范围的消息数据。SFM层还充当ODD检查器。基于ODD传感器输出，它可以检测驾驶情况何时发生变化并触发必要的AD系统模式转换，以避免不安全地使用性能有限的组件，例如AD系统感知子系统中的神经网络。

f) 控制器安全机制(CSM)层：图1中的每个片上系统(SoC)都标记为功能控制器，并具有专用的CSM层。具有车辆控制功能的SoC称为车辆控制(VC)功能控制器。其他称为非车辆控制(NVC)功能控制器。NVC CSM仅监控其本地SFM层、硬件和虚拟机管理程序；VC CSM监控所有VC和NVC功能控制器以及VSM层。CSM层可以访问主网络通道，并可以向车辆执行器发送控制命令。请注意，CSM层可以比较通道的输出以识别标称通道和安全通道之间的不一致。

g) 车辆安全机制(VSM)层：VSM层在单独的安全控制器上运行。它监控 VC CSM、安全传感器数据和两个片外网络。VSM层可以使用安全传感器数据通过辅助网络操纵车辆。此外，我们假设VSM层可以访问电源管理IC。

h) 片上网络(NoC)。NoC是SoC上硬件知识产权(IP)模块的低延迟通信互连。

i) 主网络：这是用于AD系统标称控制的高性能网络通道。

j) 辅助网络：主网络的热备用是用于车辆安全控制的异构高性能冗余通信通道。

3.2 具有成本效益的故障运行架构

在本文的范围内，我们无法提供有关我们提出的方法的成本效益的经验证据。但是，我们能够定性地将我们的方法与其他众所周知的模式进行比较。三重模块冗余(TMR)设计模式通常用于航空航天系统，例如波音777飞机飞行控制系统。TMR由三个昂贵的冗余通道和一个可靠的投票器组成。这种模式提供了高度的故障弹性并且可以进行故障运行，但是，TMR对于AD系统来说太昂贵了。我们提出的模式在标称通道中添加了更简单、更便宜的紧急和安全通道。基于系统健康状态和环境意识，DSM采用降级策略在通道之间切换，这将在第5节中描述。最简单的紧急通道根本不使用传感器，只是停止车辆。与标准通道相比，我们的安全通道依靠更简单的算法和更少的安全传感器来操纵车辆，从而降低了引入冗余的开发成本。此外，这种模式不假设额外的硬件来实现功能冗余，这有助于降低生产成本。此外，通过将安全责任分配给VSM层，功能控制器所需的完整性更低，这有助于降低相关成本。

04.故障检测与诊断

由于其分布式特性，DSM可以通过监控自动驾驶系统的SoC、网络和分布式软件来有效地检测和诊断各种故障模型。在本节中，我们讨论了DSM各层在监控故障模型方面的职责。表1列出了DSM各层可用于检测系统故障的故障模型示例以及监控技术。系统组件列涵盖了自动驾驶的整个车辆基础设施，包括传感器、执行器、处理器和网络。故障模型和性能限制的示例根据DFA（相关失效分析）耦合因子类进行分类。例如，由于机器学习实施限制，当无故障AD系统无法安全地处理道路情况时，性能限制会引发危害。请注意，所呈现的故障模型并不全面，而是举例说明了DSM层的责任范围。此外，监控技术栏还包括系统如何检测或缓解相应故障模型的示例。几种监控技术（例如心跳和消息速率监控）依赖于中间件软件来实现DSM和AD功能的分布式协调。最后，指定负责的DSM层以及最低要求的安全完整性等级的指示。

表1.示例故障模型和监测技术在DSM各层的分配

SFM层的主要职责是监控AD和ODD传感器以及AD功能，例如定位、感知和路径规划。现代智能传感器集成了复杂的车载处理和网络。因此，它们的失效模式包括通信问题（例如消息发布速率抖动）、软件问题（例如错误的自车定位）以及算法的性能限制（例如幽灵和遗漏物体）。运行AD功能的ECU、SoC和VM将表现出类似的故障模型。监控和缓解技术的示例包括消息速率监控、多模态传感器的数据融合以及与独立安全通道的比较。此外，由于SFM层与在同一强大的VM中运行的 FUN 层距离很近，因此它可以对AD功能的健康状况执行快速复杂的诊断。例如，它可以跟踪已发布数据包的时间和优先级，使用范围内和范围外检查数据包内容，检查驱动程序、操作系统内核等。

CSM层负责监控功能控制器(SoC)和VSM中的故障。每个SoC和低级软件（例如虚拟机管理程序）都可能遭受各种失效模式：片上内存损坏、处理器核心和NoC中的卡住故障、虚拟机管理程序隔离失效、固件死锁或优先级反转。这些故障模型通常发生在共享SoC资源中，并影响AD系统功能更高级别的多个组件。因此，处理这些故障模型需要比SFM层更高的完整性级别。除了表1中提到的监控技术外，CSM还可以部署片上硬件监视器，用于时钟抖动、IO错误、控制流监控和锁步处理以及数据传输。

在我们的DSM中，VC CSM使用质询-响应协议监控所有其他NVC功能控制器。质询-响应协议在传统的带看门狗的活跃心跳之上涵盖了与内存和处理器相关的故障模型。此外，当安全控制器上的VSM层发生故障时，CSM还可用作故障转移机制。为了检测VSM的无故障失效，CSM只需使用看门狗监控VSM心跳即可。CSM只能通过与实现AD功能的所有完全运行的FUN层合作来安全地操纵车辆。如果没有完全运行的FUN层，CSM只能通过紧急通道向车辆执行器发送基本的紧急停止命令。除了虚拟化和隔离之外，在功能控制器上实施虚拟机管理程序还允许CSM层在检测到故障或危害情况时快速暂停虚拟机。

整体车辆安全由高完整性VSM层管理。除了监控类似于CSM的自身安全控制器外，它还负责检查VC CSM、执行器、数据和电源网络的健康状况。转向、制动和加速执行器与智能传感器共享其（健康）状态。VSM会持续分析此状态。此外，VSM通过观察数据包传输和查询网络网关和交换机来主动监控数据网络。除了检查未满足的实时截止时间外，VSM还可以分析消息优先级和内容。最后，VSM可以控制配电网络和电源管理IC，以便在必要时关闭VC CSM、传感器和网络。

值得注意的是，除了检查AD系统功能外，DSM还会监控其自身组件是否发生故障，并具有多种故障转移降级模式来应对其所有层中的故障。多个SFM和CSM层可以任意发生故障，因此仅具有低和中等安全完整性要求，这有助于降低总体开发成本、硅片面积和功耗。但是，具有适度计算和网络要求的VSM层确实需要高完整性级别才能可靠地管理AD系统中的其他安全层。

图2：DSM降级政策

05.降级运行模式

当 AD系统处于无故障的标称模式时，VC FUN层正在控制车辆。所有安全层同时执行不同的监控任务。一旦任何安全层检测到故障，DSM就会根据当前AD系统状态激活降级运行模式。

我们在DSM中考虑了五种运行模式：标称、绕行、舒适停车、安全停车和紧急停车。模式之间的降级策略如图2所示。在该图中，每个转换上的标签代表降级的触发因素；“AD可用性”表示AD系统功能的可用性；“舒适度”表示乘客舒适度，这取决于运行期间的AD可用性；“弹性”表示车辆的容错能力。在以下小节中，我们将描述每种运行模式下的DSM行为。

5.1 标称模式

图3说明了在无故障标称模式下，带有DSM的AD系统的行为。在此模式下，所有AD系统组件均完全正常运行。车辆由标称通道中的VC FUN层控制。同时，安全通道处于热备用状态。VSM层通过辅助网络通道接收和监控安全传感器数据，但不向执行器发送任何控制命令。安全层之间的所有类型的监控也在进行中：

a) 所有AD传感器、ODD传感器和FUN层均由相应的SFM层监控。安全传感器由VSM层监控。

b) 每个SFM层和NoC由同一功能控制器上的CSMlayer监控。

c) 所有NVC功能控制器均由VC CSM层监控（为简单起见，图3中未显示）。

d) VSM层监控两个网络。

e）VC CSM和VSM层通过主网络使用质询-响应协议相互监视。

图3：分布式安全机制的无故障标称模式

5.2 绕行模式

在绕行模式下，AD系统标称通道完全正常运行。检测到安全通道故障后，VC CSM层能够让车辆绕行到最近的汽车修理厂，而不会牺牲乘客的舒适度。由于标称通道中的监控活动正常工作，如果在标称通道中检测到故障或危害情况，AD系统可以进一步降级到紧急停止模式，如图2所示。

5.3 舒适停止模式

AD系统安全通道完全正常运行，但在舒适停止模式下仅使用安全传感器。安全通道中的VSM层可以控制车辆优雅地靠边，并确保足够的乘客舒适度。如图2所示，在此模式下，当VSM检测到主网络或VC CSM中的故障时，AD系统可以进一步降级到安全停止模式，或者当VC CSM检测到VSM故障时，降级到紧急停止模式。

5.4 安全停止模式

在此模式下，AD系统安全通道仍可完全运行，但由于VC CSM故障或主网络故障，标称通道无法再执行任何降级模式，如图2所示。由于我们假设功能控制器上的组件是任意故障，因此为了执行安全停止，VSM 首先关闭VC功能控制器以防止其产生任何任意输出，然后启动安全停止程序以快速将车辆靠边，甚至在必要时执行车道内停止。我们假设在此模式下车辆立即处于安全状态。

5.5 紧急停止模式

可以通过从绕行模式或舒适停止模式降级来达到紧急停止模式。在此模式下，AD系统标称通道仅部分运行，这意味着VC CSM没有高级绕行操作所需的所有信息，但仍可以通过主网络控制车辆。此外，由于VSM或安全传感器故障，如图2所示，紧急停止模式下的AD系统安全通道无法再执行任何降级。因此，VC CSM只是向车辆执行器发送制动命令，以盲目地尽快停止车辆。显然，在此过程中无法保证乘客的舒适度。我们假设车辆在此模式下立即处于安全状态。

5.6 示例用例

如图2所示，AD系统可以首先从标称模式降级到舒适停止模式，然后降级到紧急停止模式。这种用例如图4所示。首先，AD传感器发生故障。请注意，任意故障AD传感器可以向FUN层提供任意输出，从而导致任意FUN控制输出。但是，如果安全机制迅速抑制故障控制，则故障控制可以到达车辆执行器而不会违反安全目标。在这种情况下，SFM层检测到AD传感器故障，但在SFM层能够向CSM层报告之前，SFM层发生了第二个故障。尽管如此，CSM层还是检测到了SFM层故障，并通过关闭故障SFM层正在运行的车辆控制VM来对此做出反应，然后将VM状态报告给VSM层。然后，VSM层将AD系统降级为舒适停止模式。然而，在车辆达到安全状态之前，VSM层发生了第三个故障。得益于质询-响应监控技术，CSM层检测到VSM层的故障静默故障，并进一步将AD系统降级为紧急停止模式。

图4：三点故障处理：首先是AD传感器故障，然后是功能监视器故障，再是车辆安全机制故障

在图5中，我们演示了DSM如何处理SOTIF场景。在这种情况下，当没有系统故障时，AD系统从标称模式降级为舒适停止模式，但SFM层上的ODD检查器检测到ODD已发生变化，无法保证AD系统的充分性能。

图5：离开操作设计域时SOTIF场景的处理

06.模型和形式验证

随着AD系统的复杂性不断增加，传统的安全分析（如失效模式和影响分析(FMEA)、FTA）以及道路测试和模拟方法已不足以保证AD系统的正确性，因为无法详尽地分析或测试众多系统状态。然而，建模和形式验证可以详尽且数学地证明AD系统模型所需的安全属性。这有助于减少早期设计阶段的规范和需求错误。此外，可以从形式验证的模型生成可认证代码。可执行模型可以作为整个产品生命周期的黄金参考，并有助于澄清设计利益相关者之间的沟通。

在这项工作中，我们使用mCRL2形式规范语言对图1所示的DSM架构进行建模，并在模态µ演算中形式化模型的安全要求。图1中的每个组件都被建模为有限状态机(FSM)。FSM转换指定了监控和故障处理程序中的DSM行为，如图2中的高级降级策略图和图3至图5中的序列图所示。

该模型由746行mCRL2代码和71行µ-演算公式组成。mCRL2模型也是可执行的，其行为可以在mCRL2模拟器中轻松模拟。表2显示了我们DSM模型中每个FSM的状态空间。AD系统模型让所有这些FSM并行运行，从而产生超过200万个状态和20亿个转换的状态空间。mCRL2工具能够从数学上证明该模型的属性，而使用传统道路测试或AD模拟设置来详尽测试所有这些转换则很困难。在以下小节中，我们将介绍DSM模型的详细信息。

表2.DSM状态机的状态空间

6.1 模型规范

AD系统组件使用实现发布-订阅模式的软件中间件堆栈进行通信。因此，正确建模发布-订阅通信行为至关重要。在我们的DSM模型中，信息以消息的形式共享。同一网络上的任何参与者都可以通过订阅消息主题来接收消息。我们在DSM中建模了两种类型的网络，即NoC和片外网络。DSM层使用三种消息类型进行通信：

1. 传感器数据消息。这些消息包含在AD系统中传达的传感器数据。

2. 车辆控制命令消息。这些控制命令由VC FUN层、VC CSM层或VSM层发送到车辆执行器。

3. 诊断消息。这些消息报告受监控组件的状态。

所有消息都由一个带有四个标识参数的操作组成。例如，车辆控制CMS层通过主网络通道发送诊断消息，报告车辆控制VM已关闭的操作建模为：send(VC, VM_VC, VC_VM_OFF, primary)。

表3中解释了从左到右的四个参数。对于传感器数据通信，cid和vid标识接收器组件。对于电源管理操作，网络设置为电源。使用相同结构建模的操作包括通过片外网络进行通信的发送和接收，以及通过NoC进行通信的NoCsend和NoCreceive。

表3.消息参数及示例

所有AD系统行为均由模型中的操作建模。我们在此提供几个示例：

·network_ingress、network_egress：网络通信的入口和出口阶段。

·fault_injecƟ on_*：这些操作模拟故障的发生。*可以由任何目标组件替换。图4和图5中红色标签旁边的事件属于此类型。

·vc_csm_shuts_off_vc_vm：这些操作模拟VC CSM关闭其管理的VC VM。它在图4中显示为“关闭VM”。

·vsm_powers_off_vc_controller：此操作模拟VSM层关闭VC CSM SoC。

6.2 模型假设

我们做出了以下模型假设，以明确我们研究的范围，并使模型足够小以便可验证，同时保持模型的相关性：

a) 所有故障都是永久性的、原子性的、不安全的，并且始终会被检测到。可以使用适当的监控技术来改进故障检测，而不会损害模型。瞬态故障超出了本研究的范围。

b) NoC具有无限容量，以原子方式传输数据并且永远不会发生故障。请注意，由于我们的DSM概念中的分层架构，AD系统中的不同监视器可以检测到NoC中的故障。但NoC中的故障处理是我们未来工作的一部分。

c) 电源永远不会发生故障。AD系统部分中的功率损耗可以通过各种方法（如心跳监控或质询-响应机制）检测到，因此由于DSM概念的分层结构，可以通过降级模式来缓解。但是，电源管理通常不在我们的范围内。

d) 次级网络永远不会发生故障，并且只能由安全传感器、VSM和执行器访问。我们假设安全通道中的次级网络比标准通道更可靠，因为它的实现不同且更简单，功能有限。

e) 所有DSM转换都是瞬时的，不会发生故障。

f) VSM、安全传感器和两个片外网络都是无故障的，所有其他组件都是任意故障的。

g) 通过片外主网络和次级网络的通信分为入口和出口阶段，并具有3条消息的缓冲区。出口消息以随机顺序发送。我们将缓冲区大小设置为3，以模拟无序的入口和出口数据流并保持状态空间较小。

h) 只允许某些多点故障组合，如图2所示，这样总是有一种降级模式可用于将车辆置于安全状态。

6.3 安全要求和形式属性

DSM模型安全要求如下：

要求1 AD系统无死锁；

要求2 车辆控制中始终只有一个无故障部件；

要求3 AD系统标称模式在必要时始终降级为绕行、舒适停止或安全停止；

要求4 必要时绕行必须降级为紧急停止；

要求5 必要时舒适停止必须相应地降级为安全停止或紧急停止。

DSM安全要求使用模态µ演算公式形式化。下面我们展示两个示例：

6.4 验证结果

建模和验证过程有助于减少DSM设计中的规范错误，这些错误很难手动或道路测试中检测到。例如，我们的DSM模型的早期版本将网络缓冲区大小设置为3，其状态空间为2.15亿个状态和29.2亿个转换。在使用mCRL2工具集连续10多天运行验证过程后，我们发现此模型中存在死锁。值得注意的是，当网络缓冲区大小设置为1和2时，同一模型被验证为满足所有安全要求。我们通过在不同故障处理过程中逐步执行FSM转换来调试该问题。在mCRL2模拟器的帮助下，我们很快发现死锁发生在主网络被VSM发送的有关安全传感器故障的诊断完全占用时，同时VC CSM检测到VSM故障并尝试通过完全占用的主网络激活绕行模式。然而，在之前验证的模型中，由于缓冲区较小，诊断缓冲时间不够长，不足以触发死锁。通过在VC CSM过程中添加缺失的转换，以允许它在车辆控制命令尚未发出时从VSM层接收诊断，解决了这个问题。

最终的DSM模型配置有两个功能控制器，每个控制器运行两个VM，网络缓冲区大小设置为3，从而产生超过10亿个状态和100亿个转换的状态空间。最终模型的所有安全要求都经过验证，在强大的服务器上运行了几天。虽然正式模型和实际系统实现之间总是存在现实差距，但正式方法有助于减少规范错误，通过在昂贵的AD系统实现和现场测试之前的早期设计阶段，以数学和详尽的方式证明仲裁逻辑的正确性。

07.结论

我们的工作提出了一种故障运行安全概念，结合了故障处理、性能限制缓解和驾驶决策的安全措施。采用的安全机制可处理AD系统和安全机制本身中的多点故障。所提出的AD系统架构通过使用大多数故障任意组件以及比标称通道更简单的额外紧急和安全通道来实现成本效益。基于AD系统健康状况和态势感知，在多个SoC和虚拟机上运行的DSM可激活自动驾驶的各种降级模式，以尽可能保证车辆的安全。此外，我们还介绍了将故障模型分配到安全机制层的示例，并讨论了检测故障和ODD变化的监控技术。为了减少规范错误，我们使用mCRL2语言对DSM仲裁逻辑进行了建模，并在µ-calculus中正式验证了五项安全要求。我们经过正式验证的高弹性安全概念可以作为AD系统的整体设计模式，从而最大限度地减少道路死亡人数并减少昂贵的测试。

未来有希望的研究方向包括建模时间属性、使用概率模型计算失效率、处理瞬态故障以及量化所提出的安全概念的成本效益。

标签：CSM,AD,故障,验证,形式化,安全,DSM,VSM
From： https://blog.csdn.net/NEON7788/article/details/140991197