CPS 验证

在一个智能机器日益管理我们世界的时代——从自动驾驶汽车和电网到性命攸关的医疗设备——我们如何能确定它们将安全可靠地运行？问题不再是我们能否构建如此复杂的信息物理系统（CPS），而是我们能否信任它们。从希望走向数学上的确定性是现代工程的核心挑战，而这正是通过形式化验证这门严谨的学科来解决的。该领域提供了以逻辑精度证明系统将按预期运行的工具。

本文探讨了 CPS 验证的核心原理和应用。它在对“信任”的抽象需求与实现信任所需的具体工程实践之间架起了一座桥梁。在接下来的章节中，您将对这一关键领域获得全面的理解。我们将从“原理与机制”开始，探索基础概念，在此我们将剖析让我们能够规约和表示系统行为的形式化语言（如时序逻辑）和数学模型（如混合自动机）。之后，“应用与跨学科联系”将展示这些理论工具如何应用于解决现实世界的挑战，确保网络通信的安全、自动驾驶车辆的安全，乃至人工智能驱动组件的可信度。

我们如何信任那些运行我们世界的机器？当一辆自动驾驶汽车在繁忙的十字路口穿行，一个电网在整个大陆上平衡供需，或者一个医疗设备提供维持生命的治疗时，我们如何从希望它能工作，转变为知道它能工作？对确定性的追求是构建信息物理系统（CPS）的核心挑战，而这一追求催生了一个优美而强大的数学和计算机科学领域：形式化验证。

在我们建立确定性的堡垒之前，我们必须首先清楚我们想要证明什么。想象一下，我们设计并制造了一架复杂的自主无人机。我们面临两个根本不同但同等重要的问题。

首先：“我们是否在正确地构建系统？”这是​​验证（verification）​​的问题。它询问我们构建的产物——代码、电路、物理组件——是否忠实地实现了我们设计的蓝图。这是一个内部一致性检查的过程。我们的代码 $I$ 是否符合其设计模型 $M$（$I \preceq M$）？该设计模型是否满足我们写下的形式化规约 $\Sigma$（$M \models \Sigma$）？这是一个逻辑和数学的世界，在这里我们可以做出​​演绎​​性的论断。如果我们的前提是正确的，逻辑是健全的，那么我们关于系统相对于其规约的正确性的结论是有保证的。验证就像一个细致的编辑，对照作者的最终草稿检查手稿，确保没有拼写或语法错误。它确保文本完全是作者所意图的。

其次：“我们是否在构建正确的系统？”这是​​确认（validation）​​的问题。它询问我们的蓝图和最终产品是否真的适用于真实世界。我们的无人机空气动力学模型 $M$ 是否是真实物理设备 $P$ 的精确表示？($M \approx_D^U$) 这是一个​​归纳​​性的和经验性的问题。我们必须进行实验，收集数据，并使用统计学来论证我们的模型对于其预期目的是足够的。确认就像是问手稿中的故事，即使写得再完美，是否真的对读者有吸引力和说服力。它将我们的形式世界与混乱、不可预测的物理世界联系起来。

本章深入探讨​​验证​​的世界。我们将假设确认这项困难的工作已经为我们提供了一个可信的模型和一个有意义的规约。我们的任务是探索用数学的确定性来证明我们的系统将遵守该规约的原理和机制。

那么，我们如何开始验证一个系统呢？最直观的方法是测试。我们可以在模拟器中运行我们的无人机一千个小时，如果它从未坠毁，我们的信心就会增加。但这是否证明了它永远不会坠毁？

考虑一个简单的安全需求：“对于无人机可能遇到的​​所有​​可能的阵风，在​​所有​​时间，其高度​​绝不能​​低于10米。”这是一个​​全称陈述​​。所有时间内的所有可能阵风的空间是不可数无限的。我们永远无法测试所有情况。一百万次成功的测试，甚至十亿次，仍然不能构成一个证明。你只确认了系统在你测试的那些特定场景下是安全的。

在这里，我们遇到了一个深刻的逻辑不对称性，这是由哲学家 Karl Popper 倡导的科学方法的基石。虽然你永远无法通过有限的测试来明确证明一个全称陈述，但你可以通过一次观测来明确地证伪它。要证伪绝对安全的主张，你只需要找到​​一个​​输入信号——一个特定的风阵序列 $u^{\star}$——导致无人机在某个时间 $t^{\star}$ 高度降至10米以下。这个单一的违规轨迹被称为​​反例（counterexample）​​。

​​证伪（falsification）​​的目标是智能地搜索这样一个反例。然而，​​形式化验证（formal verification）​​的目标更为宏大。它试图证明不存在这样的反例，而无需测试每一种情况。这是一次进入无限的旅程，以逻辑为武器。

在我们能证明一个属性之前，我们必须首先以完美的清晰度陈述它。日常语言太过模糊。“最终”是什么意思？“总是”有多长？​​时序逻辑（Temporal logic）​​提供了一种形式化语言，用来表达系统随时间演化的属性。

两个最基本的算子是 $\mathbf{G}$，表示​​全局地（Globally）​​（或“总是”），和 $\mathbf{F}$，表示​​最终地（Finally）​​（或“最终”）。

• $\mathbf{G}(\text{altitude} \ge 10)$: 高度总是大于或等于10。这是一个经典的​​安全性（safety）​​属性：“坏事永远不会发生”。
• $\mathbf{F}(\text{destination\_reached})$: 无人机将最终到达其目的地。这是一个经典的​​活性（liveness）​​属性：“好事最终会发生”。

针对不同类型的系统，人们开发了不同的逻辑。​​线性时序逻辑（LTL）​​和​​计算树逻辑（CTL）​​是基础性的，它们对离散事件序列进行推理，并对属性是否成立给出一个简单的布尔值真/假答案。

但对于生活在温度和电压等连续信号世界中的 CPS，我们需要更具表达力的东西。​​度量时序逻辑（MTL）​​通过为算子添加时间界限来扩展 LTL。例如，$\mathbf{G}_{[0, 5]}(\text{temperature} \ge 1)$ 表示在最初的5秒内，温度必须保持在1度以上。

一个更强大的工具是​​信号时序逻辑（STL）​​。STL 不仅仅给出一个真/假的答案，而是提供一个实数值的​​鲁棒性（robustness）​​分数 $\rho$。

• 如果 $\rho > 0$，属性被满足，$\rho$ 的值告诉我们安全的裕度。对于公式 $\mathbf{G}_{[0,5]}(x(t) \ge 1)$，鲁棒性为 $\rho = 0.5$ 意味着信号 $x(t)$ 在整个时间间隔内至少比阈值 $1$ 高出 $0.5$ 个单位。
• 如果 $\rho 0$，属性被违反。$|\rho|$ 的大小告诉我们违反了多少。鲁棒性为 $\rho = -0.2$ 意味着在某个时刻，信号下降到 $0.8$，比要求的阈值低了 $0.2$。

这种量化反馈对工程学来说是革命性的。它不仅告诉我们系统是否失败，还告诉我们失败得有多严重，为重新设计提供了宝贵的指导。

要验证一个属性，我们需要系统本身的一个数学表示——一个能捕捉其本质行为的模型。对于 CPS 而言，​​混合自动机（hybrid automaton）​​是实现这一目标的完美工具。

想象混合自动机是一个棋子在复杂棋盘上移动的规则手册。这个模型优雅地融合了物理学的连续世界和计算机控制的离散世界。

• ​​离散位置 ($L$)​​: 棋盘被划分为一组有限的命名区域，称为位置或模式。对于一个恒温器系统，这些可能是 加热、制冷 和 空闲。
• ​​连续流 ($F$)​​: 在每个位置内，代表系统连续状态（例如，温度 $x$）的棋子位置根据物理定律演化。这就是​​流（flow）​​，通常由一个微分方程描述，如 $\dot{x} = f_{\text{Heating}}(x)$。
• ​​不变量 ($I$)​​: 棋子不能自由漫游。每个位置都有一个​​不变量（invariant）​​集，一个棋子必须停留其中的“安全区”。例如，加热 模式可能只在温度低于22°C（$x \le 22$）时激活。如果状态达到不变量的边界，它将被迫进行一次离散跳转。
• ​​离散转换 ($E, G, R$)​​: 棋子可以沿着预定义的边在位置之间跳转。只有当棋子处于​​守卫（guard）​​集 ($G$) 上时才允许跳转。例如，从 空闲 到 加热 的跳转可能由守卫 $x \le 20$ 启用。当跳转发生时，状态可以通过​​重置（reset）​​映射 ($R$) 瞬时改变。例如，控制器的内部计时器可能会被重置为零。

这套简单的规则——流、跳转、不变量、守卫、重置——强大到足以模型化范围极广的系统，从简单的恒温器到庞大、互联的智能电网。

我们现在有了用时序逻辑写成的规约 $\varphi$，以及我们的系统模型——混合自动机 $\mathcal{H}$。最终的问题是：$\mathcal{H}$ 是否满足 $\varphi$，写作 $\mathcal{H} \models \varphi$？回答这个问题有两种主要哲学。

第一种是​​模型检测（model checking）​​。把模型检测器想象成一个不知疲倦的自动化探险家。它将混合自动机视为定义了一个巨大、通常是无限的状态空间迷宫。模型检测器的工作是系统地探索这个迷宫中的每一条可能路径，以确定是否有任何路径通向违反 $\varphi$ 的“不安全”配置。当然，对于一个无限的迷宫，直接这样做是不可能的。因此，模型检测器使用了非常聪明的技术，如​​抽象（abstraction）​​，它们分析一个简化的、有限的迷宫“地图”，该地图保守地捕捉了其所有基本特征。模型检测的美妙之处在于其自动化。你提供模型和规约，按下一个按钮，然后等待。如果属性为假，它会返回一个反例——通向失败的迷宫中的精确路径。

第二种是​​定理证明（theorem proving）​​。把定理证明器想象成一个聪明的逻辑侦探，由一台在推理上从不出错的计算机辅助。侦探不是去探索迷宫，而是试图证明一个定理，比如“从入口出发的任何路径都永远无法到达牛头怪的巢穴”。这种方法不是全自动的；它需要人类的洞察力来构思证明的关键步骤。人类可能会提出一个关键的引理，称为​​不变量（invariant）​​：“所有可达路径都局限于迷宫的西翼。”然后，定理证明器使用逻辑和数学的公理来严格检查这个不变量是否成立，以及它是否足以证明整体的安全性属性。虽然它要求更多的专业知识，但定理证明可以处理对于全自动探索来说过于复杂的系统类别。

让我们更深入地探讨验证中最优雅的思想之一，它可以被模型检测器和定理证明器共同使用：​​屏障证书（barrier certificate）​​。

想象我们的安全集 $\mathcal{S}$ 是一个山谷。我们想证明我们的系统，表示为一个在地形上滚动的球，如果从内部开始，就永远不会逃离这个山谷。我们如何能在不模拟每一条可能路径的情况下证明这一点？屏障证书提供了一种非常简单的方法。我们需要找到一个特殊的函数 $B(x)$，它定义了地形，使得 $\mathcal{S}$ 恰好是 $B(x) \le 0$ 的点集。如果这个函数满足三个条件，它就是一个有效的屏障证书：

1. ​​初始化​​：系统从山谷内部开始。初始状态集 $\mathcal{X}_0$ 必须是 $\mathcal{S}$ 的子集。
2. ​​流条件​​：在山谷的边界上（其中 $B(x) = 0$），地形必须总是朝向内部或水平。系统的动态 $f(x)$ 绝不能指向“上坡”。在数学上，沿着任何轨迹的 $B$ 的变化率必须是非正的：$\nabla B(x) \cdot f(x) \le 0$。
3. ​​跳转条件​​：如果系统有离散跳转（比如传送门），它们绝不能将球从山谷内部传送到外部。如果 $x$ 在山谷中，其跳转后的状态 $g(x)$ 也必须在山谷中：$B(g(x)) \le 0$。

如果我们能找到这样一个函数 $B(x)$，我们就得到了一个简单的、静态的、对所有时间都有效的安全“证书”。这是一个深刻的转变，从对无限轨迹的推理转变为检查一组代数不等式。

这似乎近乎神奇。我们总能找到这样的证书，或者总能判定一个系统是否安全吗？答案是在20世纪下半叶发现的，是计算机科学中最深刻的结果之一：不。对于某些类别的系统，安全问题是​​不可判定的（undecidable）​​。对于一个简单的​​计时自动机（Timed Automaton）​​，其中唯一的连续动态是时钟以恒定速率滴答作响，可达性是可判定的。但一旦我们允许即使是简单的非线性动态（例如，多项式方程），混合自动机就能变得足够强大，以模拟一个通用图灵机。在这种情况下，询问它是否能达到一个不安全的状态就变得等同于著名的、无解的停机问题。没有通用的算法能够为所有此类系统提供“是”或“否”的答案。系统的物理特性本身就可以执行一个其结果在根本上是预先不可知的计算。

即使对于可判定的系统，我们也面临一个强大的实际敌人：​​维度灾难（curse of dimensionality）​​。模型检测器必须探索的状态空间大小随着系统中变量和组件数量的增加而呈指数级增长。

考虑两个事件 $p$ 和 $q$ 的一个简单规约：“p 无限频繁地发生 ($G F p$) 并且 $q$ 最终永远为真 ($F G q$)。”如果我们构建一个自动机来检查第一部分，它可能只需要2个状态。第二部分可能需要3个状态。但要检查它们的合取，我们必须构造一个乘积自动机，其状态数是其组件状态数的乘积。这个自动机将有 $2 \times 3 = 6$ 个状态。要将其转换为大多数工具可以使用的标准机器，状态数可能会再次翻倍至12个。这种乘法爆炸意味着，整体地（一次性地）分析一个只有十几个组件的系统在计算上是不可能的。

唯一的前进方向是一种被称为​​组合验证（compositional verification）​​的“分而治之”策略。我们不是分析一个巨大的、整体的系统，而是将其分解为其组成部分并单独分析它们。关键是使用​​假设-保证合约（assume-guarantee contracts）​​来推理它们的交互。我们可能会在假设其传感器输入将保持在某个范围内的前提下验证控制器模块。然后我们必须单独验证传感器模块保证其输出确实会保持在该范围内。真实系统可能会表现出我们忽略的行为，导致灾难性故障。

这种方法很强大，但它带有一个关于可靠性的关键警告。在推理一个组件时，我们对其环境的假设必须是其邻居所有可能行为的保守​​过近似（over-approximation）​​。如果我们做出一个过于乐观的假设——一个忽略了某些可能（也许是恶意的或意外的）行为的​​欠近似（under-approximation）​​——我们的验证就毫无价值。我们可能证明了控制器是安全的，但这个证明是无效的，因为它的前提是错误的。真实系统可能会表现出我们忽略的行为，导致灾难性故障。

确保这些合约既足够紧密以至于有用，又足够宽松以至于可靠，是现代 CPS 验证的前沿。这就是我们如何逐步建立对我们所依赖的日益复杂的机器的信任，将工程的艺术转变为一门确定性的科学。

在我们穿越了验证的原理与机制之后，有人可能会问：这个由逻辑和数学构成的抽象世界，在何处与道路、工厂车间或手术室相遇？答案是，在计算机与物理世界以重要方式交互的任何地方。验证不仅仅是一项学术活动；它正是让我们能够构建值得信赖的信息物理系统的工程学科。这是一个建立证据链的过程，一条从高级承诺——“这个系统是安全的”——一直延伸到硅片中电子的复杂舞蹈和钢铁运动的连续推理线。

这项工作并非铁板一块。它是由多种方法构成的丰富织锦，是一个集结了计算机科学、控制理论和工程学数十年研究成果的工具箱。工具的选择取决于风险的大小。对于一个智能家居设备，简单的测试可能就足够了。但对于一个手术机器人或飞机的飞行控制系统，失败是不可接受的选项，我们必须动用整个武器库。在我们深入探讨这些工具经受终极考验的迷人应用之前，让我们先来探索一下这个验证与确认的“宏图”。

在工程学中，我们必须回答两个基本问题：“我们是否正确地构建了系统？”和“我们是否构建了正确的系统？”。第一个问题是​​验证（verification）​​的范畴，第二个问题是​​确认（validation）​​的范畴。验证是一个向内看的过程：我们对照为之设定的精确需求，检查我们的工程产物——我们的模型、我们的软件代码、我们的硬件设计。确认是一个向外看的过程：我们检查我们构建的系统以及我们编写的需求本身，是否适合其在真实世界中的预期用途，是否满足将使用它们的人的目标。

为了从利益相关者的目标走到一个经过确认的系统，工程师们采用了一系列技术，每种技术都在保真度、成本和保证之间提供了不同的平衡：

• ​​基于仿真的方法​​，如​​软件在环（SiL）​​和​​协同仿真​​，是第一步。在这里，我们在主计算机上运行控制器的软件，对抗一个纯数字的物理设备模型。这是早期设计阶段的宝贵工具，允许在任何硬件构建之前进行快速迭代和调试。

• ​​硬件在环（HIL）​​让我们向现实迈出了关键的一步。在 HIL 中，实际的嵌入式控制器硬件连接到一个复杂的实时模拟器，该模拟器模拟物理设备的传感器和执行器。在这里，我们可以捕捉到在纯软件仿真中无法看到的微秒级时序错误和硬件接口问题。

• ​​运行时验证（RV）​​在实际操作中充当守护天使。它部署一个“监视器”——一个从形式化规约合成的软件——实时观察系统的行为。与试图预测所有可能未来的离线方法不同，RV 检查正在发生的​​那一个​​未来，准备在系统偏离其规定的安全行为时发出警报。它基于传感器提供的部分信息进行操作，提供了一个必不可少的在线安全检查层。

• ​​形式化方法​​代表了保证的黄金标准。形式化方法不是运行有限数量的测试，而是使用数学逻辑来证明一个系统模型对于所有可能的输入和模型允许的所有可能场景都满足某个属性。这是达到最高安全完整性等级（SILs）所需近乎确定性的唯一方法，例如航空航天或医疗设备，其危险故障的可接受概率可能低于每亿小时运行一次。

构建一个可信系统的艺术在于知道如何组合这些技术，利用每一种技术来弥补其他技术的弱点，从而打造一条从最高层目标到最终经过确认的产品的完整证据链。

在信息物理系统执行其主要功能之前，它必须首先建立一个安全可靠的基础。验证在这里扮演着关键角色，确保计算和通信的基石是稳固的。

考虑一下打开设备的简单行为。如果初始启动过程可能被劫持，你如何信任它上面的任何软件？这就是​​可信启动（trusted boot）​​的问题。解决方案是一个“信任链”，其中只读存储器（Boot ROM）中一小段不可变的代码首先验证下一段软件的加密签名，然后再加载它。这第二段代码接着验证第三段，依此类推，直到整个操作系统被加载。这里的验证问题是：我们能证明这个链条是不可破解的吗？通过结合使用​​模型检测​​和​​定理证明​​，我们正可以做到这一点。工程师们创建了启动过程的一个抽象模型，其中包括一个试图篡改软件组件的对手。模型检测可以详尽地探索这个抽象模型的所有状态，以证明诸如“未经授权的代码永远不会执行”之类的属性。复杂的加密操作被抽象掉，被视为完美的“黑匣子”。然后，这些黑匣子确实是完美的（例如，哈希函数是抗碰撞的）这一假设，则通过演绎证明来单独论证，通常使用定理证明器。这种优雅的技术分层——为不同抽象层次使用合适的工具——是现代安全验证的一个标志。

一旦系统运行起来，它就必须进行通信。但即使在这里，秘密也可能以最意想不到的方式泄露。如果一个密钥包含的1比0多，一个加密操作可能会多花几毫秒的时间。一个能够精确测量这种时间差的对手——一个“侧信道”——就有可能重构密钥。为了防止这种情况，我们求助于强大的信息流原则——​​非干涉（noninterference）​​。这个想法既简单又深刻：秘密输入（如加密密钥）的改变不应在任何公共输出（如时间或网络包头）中引起可观察到的变化，除非通过我们明确允许的渠道。验证这个属性似乎很困难，因为它需要比较所有可能的秘密输入。然而，一种名为​​自组合（self-composition）​​的巧妙技术使其变得可行。我们创建一个复合系统，它并行运行我们程序的两个副本，使用相同的公共输入但两个不同的密钥。然后我们在这个组合系统上形式化地证明一个简单的安全属性：它们的可观察输出总是相同的。这确保了输出与秘密无关，从而堵住了泄露。

网络本身，作为任何分布式 CPS 的神经系统，也必须是可验证的。在具有分布式路由协议的传统网络中，行为可能复杂得令人发狂且不确定。单个配置更改可能会在网络中异步地连锁反应，造成暂时的环路或黑洞，这对于时间关键的控制系统来说可能是灾难性的。在这里，架构上的改变可能是可验证性的关键。​​软件定义网络（SDN）​​集中了网络控制，将交换机集合转变为一个单一的、可编程的、确定性的状态机。通过将每个交换机的行为抽象为有限自动机，我们可以形式化地建模整个网络的转发行为。像“制动器的控制命令绝不会被转发到信息娱乐系统”这样的属性，就变成了一个有限图上的简单可达性问题，这是模型检测器可以自动解决的问题。这是一个更深层次原则的优美例证：从一开始就为可验证性而设计，通常是通往可信系统的最有效路径。

CPS 验证的挑战与胜利在自主系统领域表现得最为明显。这些系统必须感知一个复杂且不可预测的世界，并据此安全地采取行动。

考虑一个在高速公路上紧密编队行驶的自动驾驶卡车车队。为了节省燃料，它们希望尽可能地紧随其后。但多近算太近？这不仅仅是一个物理问题；这是一个典型的信​​息物理问题。安全距离取决于卡车当前的速度（$v$）、其最大制动减速度（$a_{\mathrm{br}}$），以及至关重要的系统中“信息”部分的延迟，如通信延迟（$\tau_c$）和传感器处理时间。此外，卡车的传感器并没有给它真实的距离；它们提供的是一个带有一定有界误差（$\varepsilon$）的估计值。

形式化方法让我们能将这整个画面捕捉在一个单一、可验证的安全需求中。真实的安全停车距离是这些物理和信息参数的函数，类似于 $d_{\text{safe}} = d_0 + v \tau_c + \frac{v^2}{2 a_{\mathrm{br}}}$。然而，控制器必须根据它能感知到的信息做出决策。为了安全，它必须是悲观的。它必须假设与前方卡车的真实距离是其测量距离减去最坏情况下的传感器误差。于是，安全需求就变成了一个精确的逻辑陈述：“保守估计的可用间距必须始终大于或等于计算出的安全停车距离。”

这个陈述可以用像​​信号时序逻辑（STL）​​这样的形式化语言来编写，这种语言旨在表达物理系统的连续信号上的属性。然后，像​​可达性分析​​这样的验证工具可以采用卡车动力学及其控制器的数学模型，包括所有有界的不确定性，并探索所有可能的未来状态集。如果该工具能证明这个“可达集”永远不会与“不安全集”（间距小于所需安全距离）相交，那么对于给定的模型，我们就获得了一个形式化的安全保证——这比任何时长的道路测试所能提供的陈述都要强有力得多。

验证领域的最新、也可能是最大的挑战是人工智能，特别是深度神经网络（NN），在安全关键控制回路中的兴起。这些基于学习的组件（LECs）可以实现卓越的性能，但它们的决策过程通常是不透明的，其行为是从数据中学习而来，而不是明确编程的。我们如何能信任它们？

第一步是精确地说明我们在问什么。在这里，区分​​功能安全（functional safety）​​和​​性能（performance）​​至关重要。性能目标通常是统计性的，例如“在典型的驾驶循环中最小化平均燃料消耗”。这是我们可以通过大量测试和仿真来​​确认（validate）​​的。然而，功能安全属性是一个通用的、绝对的要求，例如“车辆在任何情况下都绝不能转向障碍物”。这样的属性不能仅通过测试来确认；它必须通过涵盖所有可能性的形式化、最坏情况分析来​​验证（verify）​​。

关于神经网络最令人担忧的发现之一是它们对​​对抗性扰动（adversarial perturbations）​​的脆弱性。对传感器输入的微小、通常人类无法察觉的改变——图像中的几个像素，激光雷达返回信号的轻微失真——都可能导致网络做出灾难性的错误。验证神经网络对此类攻击的鲁棒性是一个核心问题。攻击者的能力通常通过限制他们可以添加到输入中的扰动 $\boldsymbol{\delta}$ 的大小来建模。一个 $L_\infty$ 范数界限，$\lVert \boldsymbol{\delta} \rVert_\infty \le \varepsilon$，模拟了攻击者可以轻微改变每个传感器读数的情况，这对于传感器噪声或校准误差是物理上可信的。一个 $L_2$ 范数界限，$\lVert \boldsymbol{\delta} \rVert_2 \le \varepsilon$，模拟了对扰动总“能量”的约束，这对于功率预算有限的干扰攻击是可信的。模型的选择具有深远的影响。验证对抗 $L_\infty$ 界限的鲁棒性通常会导致更易于处理的计算问题（涉及线性约束），而验证对抗 $L_2$ 界限则不然（涉及二次约束）。这显示了威胁的物理建模与验证的数学可处理性之间的深刻相互作用。

最终，一个真实的系统必须既安全又有用。这导致了多目标验证问题。对于一个神经网络控制器，我们可能需要证明，对于​​所有​​初始状态，以及对于​​所有​​可能的扰动和模型不确定性：安全裕度始终保持在临界阈值 $\gamma$ 之上，​​并且​​最坏情况下的性能成本永远不会超过最大界限 $J_{\max}$。 这种鲁棒保证的合取是基于学习的系统验证的目标。

从保护启动时的第一行代码到保证复杂人工智能的行为，CPS 验证的应用横跨了现代技术的整个生命周期和架构。这些原理由一个共同的目标统一起来：用证明取代希望，构建不仅强大而且可证明可信的系统。随着我们的世界与智能、自主系统日益交织在一起，对可验证信任的追求不仅仅是一种跨学科的联系——它是一种社会必需。