汽车电子控制系统安全设计的形式化验证

摘 要：汽车电子控制系统已成为现代汽车的核心组成部分，因此，深入研究汽车电子控制系统安全设计和验证方法有助于提高车辆安全性能，增强车辆竞争力。本文阐述了汽车电子控制系统安全性的重要性，探讨了当前汽车电子控制系统安全设计和验证方法的局限性，以及汽车电子控制系统安全设计的形式化验证方法，形式化验证方法能够有效地在产品设计早期识别和消除潜在的问题和安全隐患，为汽车电子控制系统的安全设计和验证提供了新的思路。

关键词：汽车电子控制系统 安全设计 形式化验证方法

随着汽车电子化和智能化程度的不断提高，汽车电子控制系统在现代汽车中扮演着越来越重要的角色。传统的汽车电子控制系统安全设计和验证方法主要依赖于经验积累和大量的测试，难以全面覆盖所有可能的故障情况，无法有效应对日益复杂的安全威胁。在此背景下，形式化验证方法应运而生，它通过严格的数学模型和逻辑推理，从系统整体的安全属性和约束等宏观角度出发，可以系统地分析和验证系统的安全性，有助于在设计阶段就发现并消除潜在的设计缺陷和安全隐患。

1 汽车电子控制系统安全性的重要性

汽车电子控制系统的安全性对于保障车辆操作的可靠性和乘员的安全至关重要。随着汽车技术的发展，尤其是在自动驾驶和智能化功能日益增多的当下，汽车电子控制系统扮演了核心角色，其安全性的重要性日益凸显。

汽车电子控制系统的安全性直接关系到车辆行驶的稳定性和可靠性，这些系统涉及从发动机管理、制动系统到先进的驾驶辅助系统如自动紧急制动（AEB）乃至自动驾驶系统等多个方面。如果汽车电子控制系统存在缺陷或故障，会导致无法预测的车辆危险行为，如意外加速、误制动或者在紧急情况下无法正确做出反应，从而极大地增加发生事故的风险。因此，汽车电子控制系统的安全性，需要通过严谨的安全设计和严格的系统验证来实现，以确保系统在各种行驶条件下均可以稳定、可靠、安全地工作。

2 当前汽车电子控制系统安全设计与验证面临的挑战

尽管汽车制造商和研究机构不断努力提高电子控制系统的可靠性和安全性，但面对越来越复杂的应用场景和设计，当前的安全设计和验证方法仍存在一些局限性，这些局限性逐渐成为进一步提升系统的可靠性和稳定性，消除潜在的安全隐患的瓶颈。

2.1 基于场景测试和里程测试的验证方法

基于场景测试和里程测试的验证方法都是通过给系统输入测试样本数据（基于场景的测试更多的是指定场景作为测试样本，而基于里程的测试则是随机样本），观测输出来确认测试结果，并以样本测试结果通过概率统计方式来评价系统整体设计状态，这类基于样本的测试是从一种微观视角出发来评价系统整体状态的验证方法，在覆盖系统所有可能发生的情况方面存在一定的局限性，尤其是一些极端情况。且测试的质量依赖测试工作人员对系统需求、功能定义、内部外部交互关系等细节的准确理解，这样才能有效分析关键测试点并设计具有重要代表性的测试用例，从而提升对系统整体设计状态评价的准确性。现代汽车依赖数以百计的电子控制单元（ECU）来管理从发动机运行到自动驾驶的各种功能，在智慧交通高速发展的大背景下，这些功能需要应对越来越多样化的复杂驾驶场景，同时车辆的外部交互需求（V2X）也不断提升，系统功能和设计的复杂度与日俱增。系统复杂度的不断提升给设计工作人员准确表达系统需求和设计，以及测试工作人员充分理解系统需求和设计，分析关键测试点并设计高质量测试用例来充分验证系统满足安全约束带来的困难。

而随着基于机器学习的人工智能技术在汽车电子系统，尤其是自动驾驶系统中越来越广泛的应用，技术的迭代模式转为由数据驱动，迭代速度已不可同日而语。

自动驾驶系统已经从以往集中在驾驶辅助SAE Level 1， Level 2功能的水平向更接近自动驾驶的SAE Level 3， Level 4功能进发，这个过程中自动驾驶系统将承担越来越多的安全职责，对系统安全性的要求越来越苛刻。

汽车电子控制系统验证的不足会造成潜在缺陷和安全风险在产品上市后才被发现，给用户安全带来威胁，系统功能和设计复杂度的提升、技术迭代速度的提升、系统安全性要求的提升这三大因素互相影响，给基于场景测试和里程测试的验证方法带来了诸如场景多样性以及极端场景的稀缺性影响验证覆盖度和可实现性、仿真场景和真实场景的差异性对仿真测试结果可信度的影响、高昂的测试成本（时间，人力，财力等多方面成本）等考验[1]。行业很多研究致力于提升基于场景测试和里程测试的验证覆盖度和效率[2]。单纯依赖场景测试和里程测试的验证方法在系统验证的充分性和完整性方面，尤其针对自动驾驶系统，仍然存在一定的局限性。行业也在不断探索组合各种不同的验证方法来提升复杂安全系统验证的充分性和完整性。

2.2 设计过程中的可验证

随着系统复杂度、技术迭代速度、系统安全性要求的不断提升，对系统开发和验证的周期以及成本带来了更大的压力，我们更希望在产品开发过程中能尽早发现设计中的安全缺陷和不足，越早发现问题，解决问题的时间和经济成本越低。传统的针对设计方案验证方法有：设计评审和安全设计分析，设计评审过程中，评审人员更多凭借经验教训，结合一些设计最佳实践规则来发现方案中的问题点，而安全分析借助一些分析方法如失效模式与影响分析（FMEA），故障树分析（FTA），数据流和程序流分析结合经验以及对系统的理解，确认设计方案的正确性和完整性，设计评审和安全设计分析都高度依赖系统需求和设计所展现的信息，参与人员对系统需求和设计的充分理解以及设计经验，在面对高度复杂的系统时同样有一定局限性。

3 形式化验证方法

在汽车电子控制系统日益复杂的背景下，基于场景和里程测试，评审以及安全设计分析的验证方法在不同程度上展现出一定的局限性。形式化验证方法作为一种严格缜密的系统设计验证方法，为破局提供了一种新的思路。形式化验证方法能够在系统需求定义和设计阶段就识别和消除潜在的问题点，显著提高系统的可靠性和安全性，这种方法通过严格的数学和逻辑推理，可以全面分析系统设计模型，验证其是否满足预定的安全属性（也可以称为安全约束）。形式化验证方法理论上可以覆盖系统设计模型完整的状态空间和行为，相比较基于样本测试得到的概率统计结论以及高度依赖经验的设计评审和安全设计分析结果，能够提供更高的保证级别（Statement Reliability），尤其是处理复杂系统和关键安全属性。优势主要体现在以下几个方面：

（1）通过形式化语言（数学和逻辑的语言）能更精确表达需要满足的安全特性（安全约束），在信息表达的准确度，避免歧义和语义模糊方面明显优于自然语言，同时通过形式化表达的安全特性（安全约束）是能够被计算机所理解，能直接作为形式化验证的依据，方便实现自动化验证过程。

（2）可以在系统需求定义和设计阶段就发现缺陷和不足，有利于降低问题修复成本，提升效率。

（3）鉴于形式化验证方法理论上可以覆盖系统设计模型所有可能的状态和行为，比依赖经验的设计评审和安全分析，更有利于全面发现设计缺陷。

（4）利用形式化验证方法，可以帮助验证测试场景模型与安全特性（安全约束）的匹配程度，提升测试场景覆盖度，尤其是极端场景。

本文将探讨汽车电子控制系统安全设计的形式化验证方法，阐述其核心组成部分和工作流程。

3.1 形式化规约和建模

在汽车电子控制系统的安全设计中，形式化验证是一种重要的方法，依赖数学和逻辑上的精确描述来证明形式化规约（Formal Specification）和系统设计模型之间的匹配程度，从而验证系统设计是否符合预期的安全特性（安全约束）。形式化验证的过程如图1，涉及两个核心步骤：定义形式化规约和构建系统设计的形式化模型。

首先，定义形式化规约，形式化规约是系统需求（包括安全特性）以数学和逻辑表述方式的形式化表达，用以描述系统被期望满足的时序特性，状态迁移，功能行为，约束（包含安全约束）等方面的设计要求。而形式化语言是以数学和逻辑表述方式定义形式化规约的重要工具，例如，使用线性时态逻辑（LTL）或信号时态逻辑（STL）来表达系统时序特性，状态迁移，功能行为，约束（包含安全约束）等方面的设计要求。在形式化语言的帮助下，系统需要满足的设计要求被全面且精确地描述并形成形式化规约，规约可以被计算机所识别并成为后续形式化验证的检验标准。形式化规约的制定需基于对系统需求的全面理解，包含系统需要遵守功能规范，法规，安全约束，时间和性能限制，异常或者边界情况下的系统行为等各个方面。

其次，构建系统设计的形式化模型，这一过程中需要将系统的行为、组件和内外部接口、状态以及时序逻辑这些系统设计细节用形式化建模语言加以描述。例如，设计人员可以使用Petri网来辅助建模[3]，Petri模型能够描述系统的并发、同步、序列化等过程，不同输入条件下状态迁移行为以及时间约束。对于复杂的控制逻辑也可以采用其他建模语言如Alloy或Z语言来表达。系统设计的形式化模型不仅需要能够精确地反映系统的行为和结构，状态空间，时序逻辑等方面的设计细节，还应该包含系统可能面临的各种异常处理和边界条件，如输入错误、资源不足、输入处于上下边界、系统资源临近限制值，系统响应时间达到或超过时间限制等情况下系统的行为。

通过上述定义形式化规约和构建系统设计的形式化模型这两个步骤，为后续针对汽车电子控制系统安全设计的形式化验证做好准备。

3.2 形式化验证

形式化验证方法是一种基于数学和逻辑推理及分析来证明系统设计模型满足形式化规约的方法。常用的形式化验证方法包含模型检验（Model Checking），等效性检验（Equivalence checking），理论证明（theorem proving）等[4]。这里主要介绍模型检验，模型检验通过遍历系统设计模型所有可能的行为和状态，检查是否存在违反形式化规约的情况，主要包含两部分工作：模型正确性检验和模型一致性检验。模型正确性检验的主要目的确保系统设计模型本身不存在缺陷，依赖一些模型分析工具如Tina（和Petri适配性较好）、Simulink Design Verifier（适用于MATLAB Simulink模型）可以检查模型并帮助发现诸如逻辑无法被执行（死逻辑）、数组访问越界和整数溢出、数值超范围或有效性错误、除零等模型设计错误。

而模型的一致性检验主要的目的是验证模型与形式化规约的一致性（符合程度），不同于基于样本的测试从微观视角出发来评价整体设计状态的方式，形式化验证中，测试人员从形式化规约中提取模型的待证明特性（待证明特性可以是系统设计模型期望的输出结果或者输出结果的范围限制来验证模型的输出，也可以是包含前置条件（Pre-condition）和后置条件（Post-Condition）的逻辑表达式来验证模型的行为逻辑，或者其他期望达成的设计结果），通过遍历系统设计模型所有可能的行为和状态来寻找待证明特性的反例，如果无法找到反例，则待证明特性成立，系统设计模型满足对应的形式化规约。这种验证方法从宏观视角出发，可以覆盖模型所有可能的情况，提供更高的保证级别（Statement Reliability），同时模型检验的另一个优势是其能够提供自动化且全面准确的验证结果，大大减少人工介入的需求和相关的错误可能性。

反例分析是基于模型检验的形式化验证过程中的一个关键环节，当模型检查工具发现待证明特性不成立，它会指出对应的反例，即导致规约违反的具体事件，常见的反例有验证过程中发现特定情况下系统的输出与待证明特性不符或超过待证明特性指定的限制范围，或者在未满足前置条件（尤其安全相关的条件）的情况下系统就执行了对应动作，又或者前置条件满足（比如检测到安全故障）的情况下系统没有正确执行对应动作（比如关闭执行器并且给驾驶员警告）、执行延迟或超时等等。反例分析的主要任务是分析这些事件的路径，确定导致待证明特性不成立的原因，并提供有关如何修改设计以解决这些问题的方案，这一过程对于开发者深入理解问题产生的具体场景和原因非常重要。在进行反例分析时，设计人员需要详细检查反例提供的信息，包括违反规约的具体状态转换、相关变量的值以及触发错误的操作序列。通过这一分析，设计人员可以识别出设计中的问题，问题背后的设计错误或者性能瓶颈，并据此调整系统设计，反例的详细分析还可以帮助改进系统的测试策略，通过针对性地测试那些在模型验证中已识别为薄弱环节的部分，确保系统的整体稳定性和可靠性。

4 结束语

本文通过探讨汽车电子控制系统安全设计的形式化验证方法，为提高汽车电子系统的安全性和可靠性提供了新的思路。形式化验证方法能够有效地在产品设计早期识别和消除系统设计中潜在的问题和安全隐患，提高系统设计的效率和准确性。然而，形式化验证方法的应用仍面临着模型复杂度控制、验证效率提升等挑战，未来的研究方向应着重于优化形式化模型，提高验证算法效率，以及探索形式化验证与其他先进技术如人工智能的融合应用，为汽车产业的健康发展和用户安全保驾护航。

参考文献：

[1] W. Ding， C. Xu， M. Arief， H. Lin， B. Li， and D. Zhao， “A survey on safety-critical scenario generation for autonomous driving – a methodological perspective，” 2023.

[2] C. Amersbach and H. Winner， “Defining required and feasible test coverage for scenario-based validation of highly automated vehicles，” in 2019 IEEE Intelligent Transportation Systems Conference （ITSC）， pp. 425–430， IEEE， 2019.

[3]庞明宝，刘震.基于Petri网立交桥智能网联车协作控制仿真[J].系统仿真学报，2023，35（3）：484-493.

[4]李永明.可能LTL模型检测的两种方法[J].陕西师范大学学报（自然科学版），2014（06）：21-25.