有界模型检验

在从微处理器到生命攸关软件的复杂现代科技世界中，确保正确性是一项艰巨的任务。由于可能的状态数量比宇宙中的原子还多，传统的测试方法只能触及皮毛，使得系统容易受到那些难以捉摸的、灾难性的错误的影响。我们如何才能确信一个系统没有缺陷？本文探讨了有界模型检验（BMC），一种以逻辑精度应对这一挑战的强大形式化验证技术。我们将深入探讨 BMC 的核心原理，剖析它如何巧妙地将发现错误的问题转化为解决一个逻辑谜题。随后，我们将游历其多样化的应用，探索这个诞生于完善计算机芯片需求的方法，如今如何帮助保护智能合约、验证人工智能行为，甚至解码生命本身的逻辑。我们首先从审视有界模型检验核心的精妙机制开始。

想象你是一名侦探，但你的犯罪现场不是一间尘土飞扬的房间，而是微处理器内部那个闪闪发光、错综复杂的世界。一个错误——设计中的一个微小缺陷——已经发生，导致了灾难性的失败。但这个错误难以捉摸。它只在经历了一个包含一百万次操作的特定序列之后才会出现。你究竟要如何找到导致失败的精确事件链呢？这是当今复杂数字和信息物理系统验证工程师所面临的挑战。你不可能测试所有情况——可能性的数量比宇宙中的原子还多。你需要一个巧妙的策略。你需要一个逻辑显微镜。

这就是​​有界模型检验（BMC）​​这一优美思想的用武之地。如果我们无法检验无限多的可能性，那就让我们务实一些。让我们当一个“有界的”侦探。我们将声明，我们只调查某个特定长度内的事件序列，这个“界限”我们称之为 $k$。我们在寻找一个在 $k$ 步或更少步内出现的错误。

该方法的核心是一个极其简单的概念，称为​​展开​​。我们获取系统的蓝图——即它如何从一个时刻变化到下一个时刻的一套规则——然后我们创建一系列的时间快照。可以把它想象成一个连环画。第一个画板是系统在时间 $t=0$ 的状态。第二个画板是系统在时间 $t=1$ 的状态，依此类推，直到第 $k$ 个画板。

对于一个数字电路，“状态”就是在某个瞬间存储在其内存寄存器中的值的集合——0 和 1。“转移关系”是那套由逻辑门编码的规则，它根据当前状态和任何新输入来决定下一个时钟周期的状态。因此，展开系统仅仅意味着创建一系列变量来表示每个离散时刻的状态：$s_0, s_1, s_2, \dots, s_k$。

现在我们有了系统可能演化的连环画，我们如何对它提出问题呢？我们将整个场景翻译成逻辑的通用语言——一个单一、巨大的布尔公式。这个公式是一个宏大的谜题，如果我们能解开它，我们就找到了我们的错误。这个谜题有三个基本要素，都通过逻辑“与”(AND)运算符连接起来。

1. ​​起点​​：我们必须说明故事从哪里开始。这是​​初始条件​​，一个确定我们连环画第一帧的逻辑子句。例如，Initial(s_0) 可能表示：“计数器从零开始。”

2. ​​物理定律​​：我们必须在每一步都强制执行我们系统的规则。这就是展开的​​转移关系​​。对于从时间 $i$ 到 $i+1$ 的每一步，我们添加一个子句 Transition(s_i, s_{i+1})，表示：“时间 $i+1$ 的状态必须是时间 $i$ 状态的有效结果。”我们将这些连接起来：Transition(s_0, s_1) AND Transition(s_1, s_2) AND ... AND Transition(s_{k-1}, s_k)。这确保了我们的连环画描绘了一个物理上可能的事件序列。为了做到这一点，即便是像加法这样的算术运算也会被分解成其基本的逻辑组件——这个过程称为​​位爆破​​——使用像与、或、异或门这样的基本构建块。

3. ​​罪行​​：最后，我们必须描述我们正在寻找的错误。我们想知道一个​​坏状态​​是否可能被达到。所以我们添加一个子句，表示：“坏状态在第 0 步，或第 1 步，或 ... 或第 $k$ 步存在。”这被写成一个大的析取：$\bigvee_{j=0}^{k} \text{Bad}(s_j)$。它在问：在我们的连环画中，是否存在任何一帧发生了罪行？

把所有这些放在一起，我们的宏大谜题看起来是这样的：

$I(s_0) \land \left( \bigwedge_{i=0}^{k-1} T(s_i, s_{i+1}) \right) \land \left( \bigvee_{j=0}^{k} \text{Bad}(s_j) \right)$

这一个公式完美地捕捉了我们对错误的有界搜索。这样一个揭示错误的序列是否存在的问题，现在被归结为计算机科学中的一个著名问题：​​布尔可满足性问题（SAT）​​。我们能为这个公式中的所有变量找到一组真和假的赋值，使得整个表达式为真吗？如果能，我们就挖到金矿了。

BMC 真正的魔力不仅仅是从我们的逻辑引擎——​​SAT 求解器​​——那里得到“是”或“否”的答案。一个“是，此公式可满足”的答案还附带一个彩蛋：解本身。这个解，被称为一个​​可满足赋值​​，是谜题中每个变量的真和假值的完整列表。

但我们的变量是什么呢？它们是状态 $s_0$ 的位，输入 $i_0$ 的位，状态 $s_1$ 的位，等等，贯穿整个展开序列！所以，可满足赋值不是一个抽象的答案；它是一个具体的、逐步的系统执行轨迹。这就像侦探递给你一份罪行的录像带。

例如，求解器可能会返回一个赋值，我们可以将其解码为人类可读的报告：

• 在 $t=0$ 时：状态为 $s(0)=0$，输入为 $e(0)=1$。
• 在 $t=1$ 时：状态为 $s(1)=1$，输入为 $e(1)=1$。
• 在 $t=2$ 时：状态为 $s(2)=2$，输入为 $e(2)=1$。
• 在 $t=3$ 时：状态为 $s(3)=3$。找到了！达到了坏状态。

这就是​​反例​​。它是一个供工程师复现错误的精确配方。没有任何模糊之处。这种生成具体、可操作的错误报告的能力，使得有界模型检验成为现代工程中不可或缺的工具。

到目前为止，我们一直在寻找那种系统必须“永不进入坏状态”的错误。这些被称为​​安全性属性​​。它们就像是“坏事永不发生”形式的规则。但还有另一类更微妙的属性：​​活性属性​​。这些是“好事最终必须发生”形式的规则。例如，“如果一个进程请求资源，它最终会获得访问权限。”

在这里，我们面临一个有趣的悖论。我们这位只能预见未来 $k$ 步的有界侦探，如何可能验证一个关于“最终”的属性，而这似乎需要审视一条无限的时间线？

解决方案是一个极其优雅的想法。一个活性违例——即某个好的事情永不发生的场景——必然涉及系统陷入一个循环。这就像一个电脑程序死机，无休止地重复相同的操作序列而没有进展。要找到这样的错误，我们不寻找一条简单的路径；我们寻找一个​​套索​​：一条通向重复循环的有限路径。

我们的逻辑谜题变得更加复杂。除了通常的约束之外，我们还增加了一个​​循环约束​​，比如 $state_k = state_l$，其中 $l k$ 是某个更早的时间。这迫使路径首尾相接，形成一个循环。然后，我们检查那个“好事”是否永久地缺席于该循环。为了形式化地做到这一点，BMC 与计算机科学的另一个美丽领域——自动机理论——联手，精确定义了无限行为违反属性的含义。这揭示了逻辑和自动机这两个看似迥异的领域之间深刻而强大的统一性。

我们已经看到了 BMC 如何发现错误。但如果它没发现呢？如果 SAT 求解器对我们的公式返回“不可满足”怎么办？这意味着在界限 $k$ 内不存在错误。我们可以增加 $k$ 再试一次，但这可能很慢。一个更高级的策略是从我们系统的一个简化图景——一个​​抽象​​——开始。这就像使用一张粗略的地图而不是详细的卫星图像。搜索速度更快，但我们可能会发现一些并非真实的“错误”；它们是我们过度简化的地图的产物。这些被称为​​伪反例​​。

问题是，我们能从这些错误中学习吗？当我们发现一个伪反例时，我们就有了一个证明它不可能发生的证据。事实证明，这个“失败的证明”是一个信息金矿。来自数理逻辑的一个深刻结果，​​Craig 插值定理​​，为我们提供了一种提取这些信息的方法。

想象一下，我们将我们的伪轨迹划分为两部分：A 部分，从起点到某个中间点的路径；B 部分，从那个点到坏状态的路径。这个轨迹是伪的，因为在接口处存在冲突：没有哪个状态能同时作为 A 的有效终点和 B 的有效起点。公式 $A \land B$ 是不可满足的。

Craig 定理指出，如果 $A \land B$ 不可满足，那么必定存在一个“解释”公式，称为​​插值​​ $I$，它完全存在于接口上（它只使用 A 和 B 共享的变量）。这个插值 $I$ 有两个神奇的性质：

1. $A \Rightarrow I$：任何通过路径 A 可达的状态都必须具有属性 $I$。
2. $I \land B$ 是不可满足的：任何具有属性 $I$ 的状态都永远不能通过路径 B 导致坏状态。

插值是冲突的核心原因。例如，我们的分析可能会揭示，任何从起点开始的路径都迫使状态位 $b_1$ 在接口处为1（$A \Rightarrow b_1$），而通往错误的路径则要求 $b_1$ 为0（$B$ 要求 $\neg b_1$）。插值就是简单的 $I \equiv b_1$。这就是解释失败的“啊哈！”时刻。

这个新发现的知识，谓词 $b_1$，可以用来精化我们的抽象地图，使其更加精确。我们将这个谓词添加到我们的模型中，排除了这个特定的伪路径以及所有类似路径。这个优美的反馈循环，即失败的证明引导我们更好地理解系统，是一种称为​​反例指导的抽象求精（CEGAR）​​技术的核心。它证明了即使是我们的逻辑失败也能推动我们走向真理。

现在我们已经熟悉了有界模型检验（BMC）这台精妙的逻辑机器的运作机制，我们可能会问：它究竟有什么用？它仅仅是一个美丽的理论构造，一个供逻辑学家和计算机科学家玩的游戏吗？答案，正如科学中常有的那样，是一个响亮的“不”。这个诞生于制造完美计算机芯片这一极其现实需求的工具，已经变成了一把万能钥匙，打开了其创造者可能从未想象过的领域的大门。

在本章中，我们将游览这些意想不到的王国。我们将从 BMC 的故土——硅和电路的世界——开始，然后前往数字货币的抽象平原，信息物理系统的复杂地景，最后，到达最令人惊讶的前沿：我们细胞内错综复杂的、活生生的代码。

现代世界建立在计算机芯片之上，这些芯片是由数十亿个微观晶体管以难以想象的速度开关构成的复杂城市。这座城市中一根错位的导线，一个逻辑缺陷，都可能导致灾难——从简单的电脑崩溃到生命支持系统的灾难性故障。我们如何能确定这些设计的正确性？通过尝试几个输入来测试它们，就像只参观几栋房子来检查一个城市是否建得好一样。我们需要一种方法来检查所有情况。这正是模型检验大放异彩的地方。

想象一个复杂的处理器流水线，一个执行计算机指令的多级装配线。我们想确保它永远不会进入已知的错误状态。但如果我们关心的属性更微妙呢？如果我们想证明系统永不陷入一个无限循环，即它在做有用的工作但从未达到最终期望的状态，或者相反，它永不陷入一个“安全”的循环，从而永远避开一个必要但危险的状态？BMC 可以通过寻找一种特殊类型的反例来回答这个问题：一条“套索形”路径。这是一条从初始状态开始，运行若干步，然后循环回到自身的路径，形成一个无限重复的执行。通过要求 BMC 工具找到一个永不访问错误状态的套索，我们可以形式化地证明或证伪关于芯片无限行为的属性，这是验证其基本正确性的关键一步。

芯片设计师的关注点通常更具体，归结为时序问题。考虑你电脑中的内存，一块 DDR SDRAM。它在一套严格的时序规则下运行。其中一条规则是行激活时间，或 $t_{RAS}$，它规定了内存行在可以被“关闭”（预充电）之前必须保持“打开”的最短时间。违反这条规则可能导致数据损坏。一个内存控制器要处理多个内存库的命令，试图最大化性能。我们如何确保其复杂的调度逻辑永远不会意外地过早发出PRECHARGE命令？我们可以将控制器和内存库建模为一个状态机，并使用 BMC 展开到某个长度的所有可能命令序列。在每一步，我们检查是否在一个打开的内存库上，在 $t_{RAS}$ 个周期过去之前发出了PRECHARGE命令。如果 BMC 工具在详尽检查所有可能性后没有发现这样的序列，我们就能对我们的内存控制器遵守这一关键时序约束获得高度的信心。

在硬件设计中，也许最深刻的应用不仅仅是发现错误，而是证明正确性。假设我们有一个可行的电路设计，一位工程师提出了一个更巧妙、更优化的版本，它更快或功耗更低。我们如何知道新电路在功能上与旧电路完全相同？这就是时序等价性检验（SEC）问题。诀窍是构建一个“miter”电路，它将两个设计结合起来，为它们提供相同的输入。miter 的输出是一个比特：$m = o_1 \oplus o_2$，即两个电路输出的异或。当且仅当 miter 的输出 $m$ 总是零时，这两个电路是等价的。这将等价性问题转化为一个安全性属性检查：$G(m=0)$，即“全局地，输出总是零”。然后可以使用 BMC 来搜索任何能使 $m=1$ 的输入序列。如果在某个称为“完备性阈值”（系统状态空间的直径）的特殊界限内没有找到这样的反例，我们就不仅仅是测试了电路，而是证明了它们是等价的。这项技术如此强大，甚至可以处理像重定时和流水线这样的优化，在这些优化中，新电路的输出被有意延迟几个时钟周期。只需用相应的延迟元件调整 miter，就可以确保我们在时间上比较的是同类事物。

BMC 的精妙之处甚至延伸到验证我们给予设计工具的微妙指令。为了满足时序目标，设计师经常告诉综合工具忽略某些信号路径，将它们声明为set_false_path。这是一个承诺，即该路径在功能上是不可敏化的——无论电路的其余部分发生什么，该路径起点的信号变化永远不会影响其终点的值。一个错误的承诺可能导致综合工具产生有缺陷的芯片。我们如何检查这样的承诺？我们再次使用一个双副本 miter 模型。我们并行运行电路的两个仿真，输入和初始状态完全相同。在一个副本中，我们在问题路径的起点注入一个微小的、单周期的差异。然后我们问 BMC 工具：是否存在任何合法的输入序列，能让这个微小的差异在该路径的终点被观察到？如果工具详尽搜索后报告答案是“否”（公式不可满足），我们就形式化地证明了该路径确实是伪路径，用数学的确定性验证了设计师的直觉 [@problem_-id:4270660]。

从硬件到软件的逻辑飞跃很小。在其核心，一个计算机程序也是一个转移系统，从一个状态转移到下一个状态。模型检验在软件验证中找到肥沃的土壤是很自然的。最激动人心的现代应用之一是在区块链和智能合约的世界里。

智能合约是一个存在于区块链上的程序，通常控制着价值巨大的数字资产。智能合约中的一个错误不仅仅是不便，它可能导致数百万美元的不可逆转的损失。一个常见的要验证的属性是，合约的逻辑保持代币的总供应量不变。换句话说，任何交易或交易序列都不应能凭空创造或销毁代币。这可以表示为一个不变量：$\mathbf{G} \left( \sum_{a \in \mathcal{A}} M(a) = S_{0} \right)$，其中 $M(a)$ 是地址 $a$ 的余额，$\mathcal{A}$ 是所有地址的集合，$S_0$ 是初始总供应量。

在这里，我们面临一个巨大的挑战：地址集合 $\mathcal{A}$ 基本上是无限的。合约的状态空间是无界的，这似乎使其超出了像 BMC 这样的有限方法的范围。但在这里，形式化推理的优雅提供了一条出路。我们可以采用强大的抽象技术。一种是对称性归约。供应量守恒属性不关心地址的具体身份，只关心它们的余额。我们可以将所有地址视为可互换的，或对称的。这使我们能够分析一个更小的系统，在这个系统中我们不区分“Alice 转账给 Bob”和“Charlie 转账给 David”。另一种技术利用数据无关性。如果合约逻辑只检查两个地址是否相等，而不依赖于它们的实际比特值，我们就可以证明一个“小模型属性”。这保证了如果错误确实存在，它会在一个只有少数几个地址的小型系统中出现。通过验证这个小型的、抽象的系统，我们可以对无界的、真实世界的系统做出可靠的结论。这些抽象技术与 BMC 相结合，正处于保障蓬勃发展的去中心化金融世界的最前沿。

我们的旅程现在将我们带到数字世界与物理世界交汇的系统：信息物理系统（CPS）。这些系统驱动我们的汽车、驾驶我们的飞机、管理我们的电网。它们将软件控制器与受物理定律支配的物理设备相结合，这些物理定律由微分方程描述。验证它们是一项艰巨的任务。

想象一下汽车中的刹车系统，其动力学根据它处于“巡航”还是“刹车”模式而变化。控制器是一段软件，但系统的状态——车辆的速度 $x(t)$——是一个连续的实数。BMC 如何处理这个问题，因为它是在离散步骤上操作的？关键是再次将其与其他强大的思想结合起来。我们使用一个更高级的工具，一个可满足性模理论（SMT）求解器，它不仅理解布尔逻辑，还理解像线性实数算术（LRA）这样的理论。我们可以将连续动力学离散化为线性更新方程，如 $x_{i+1} = a x_i + b u_i$，并将这些方程，连同模式切换逻辑和安全不变量（例如 $x_i \ge 0$），编码成一个大的 SMT 公式。BMC 过程将这些混合动力学展开有限步，SMT 求解器则搜索违反安全属性的轨迹。虽然这种方法使得在有界范围内验证这类系统变得可判定，但混合系统中无界可达性的普遍问题仍然是不可判定的，这是我们在自动证明方面的一个深刻界限。

当控制器不是传统程序而是支持学习的组件（LEC），例如神经网络时，这个前沿变得更具挑战性。随着我们开始将我们的安全托付给人工智能，验证其行为的需求变得至关重要。令人惊讶的是，BMC 的原理也可以在这里得到应用。对于一个使用像 ReLU 这样的分段线性激活函数构建的神经网络，确定给定输入集的精确可能输出集的问题，可以被编码并求解，例如，作为一个混合整数线性规划（MILP）问题。这个过程，称为可达性分析，是一种有界验证形式，它为我们提供了关于神经网络控制器行为的数学保证。尽管由于指数级的复杂性它面临巨大的可扩展性挑战，但它代表了构建可证明安全的人工智能的关键第一步。

也许模型检验最惊人的应用在于一个远离硅和软件的领域：生物学。随着我们学会阅读遗传密码，我们开始看到，活细胞内复杂的相互作用网络表现得非常像一个复杂的电路。

一个基因调控网络，其中基因产生蛋白质，这些蛋白质又激活或抑制其他基因，可以被建模为一个布尔网络。每个基因的状态要么是“开”（1），要么是“关”（0），其下一个状态由其他基因当前状态的布尔函数决定。这正是模型检验为之设计的系统类型！生物学家可以将其关于网络行为的假设表述为一个时序逻辑属性——例如，“总是，如果基因 A 开启，那么基因 B 最终会关闭。”然后他们可以使用 BMC 来搜索一条“见证路径”——一个违反该属性的特定状态转换序列。如果找到，这个反例就不是一个错误；它是关于细胞动力学的一个具体的、可检验的预测，为生物机制提供了深刻的见解。

雄心不止于理解生命；它延伸到改造生命。在合成生物学中，科学家们正在重写生命的代码本身。一个巨大的挑战是重新分配密码子——我们 DNA 中指定氨基酸的三字母“单词”。想象一个计划，让终止密码子UAG编码一种新的非标准氨基酸。这需要对细胞机制进行一系列复杂的修改，包括移除通常识别UAG的蛋白质（释放因子 1）。我们如何能确定这种激进的改造是安全的？我们可以将整个翻译过程——核糖体沿着信使 RNA 移动，tRNA 携带氨基酸——建模为一个巨大的 Kripke 结构。然后我们可以在 LTL 中形式化地指定安全属性，例如：“​​G​​lobally, if the ribosome encounters a UAG codon at an unapproved site, it does not incorporate the new amino acid.”（全局地，如果核糖体在未经批准的位置遇到UAG密码子，它不会掺入新的氨基酸）。然后，一个 LTL 模型检验器可以详尽地探索在提议的遗传修饰下的所有可能的翻译场景。一个反例将精确定位导致错误的特定序列或资源配置，从而让生物学家在合成任何一个分子之前就能完善他们的计划。这是对形式化推理统一力量的终极证明——验证微处理器的相同逻辑，可以帮助我们安全地改造生命本身。

从计算机的心脏到细胞的心脏，有界模型检验的旅程揭示了一个关于科学的深刻真理。一个单一、强大的思想，诞生于实际需求，可以向外扩散，提供一个新的镜头来观察世界，一套新的工具来塑造世界。其原理很简单：在有限的界限内探索所有可能性，并以逻辑的无可辩驳的严谨性来做到这一点。它的应用，如同我们自己的好奇心一样，是无止境的。