模型检验中的对称性破缺技术：应对核电站IC系统验证的组合爆炸

1. 项目概述：当模型检验遇上核电站的“双胞胎”系统

在核电站仪表与控制（I&C）系统的设计与验证领域，我们面临着一个核心矛盾：一方面，系统必须达到近乎绝对的安全性与可靠性，任何潜在的逻辑缺陷都可能导致灾难性后果；另一方面，为了确保这种可靠性，系统设计普遍采用了冗余和对称架构，这恰恰使得对其进行穷尽性验证的计算复杂度急剧攀升，即所谓的“状态空间爆炸”问题。模型检验作为一种强大的形式化验证技术，能够通过算法自动、穷尽地检查系统模型是否满足用时态逻辑（如LTL、CTL）表述的规约。然而，面对一个由多个冗余通道、对称模块构成的复杂I&C系统，直接进行全状态空间搜索往往在计算上是不可行的。

这就引出了我们这次要深入探讨的核心技术：对称性破缺。简单来说，如果系统中有多个完全相同的“双胞胎”模块或通道，那么从验证的角度看，许多由这些对称部件不同排列组合产生的状态，在逻辑上是等价的。验证其中一个代表性组合，其结果可以推广到其他对称组合上。手动识别并利用这些对称性进行剪枝，不仅繁琐且容易出错。本文所介绍的研究工作，正是致力于将这一过程自动化、形式化，构建一套能够自动识别I&C系统模型中的对称性，并据此大幅减少需要验证的故障配置数量的方法论与工具链。这对于将模型检验真正应用于工业级、大规模核安全系统的验证，具有关键的工程实践价值。

2. 核心原理：从冗余对称设计到形式化模型剪枝

2.1 核电站I&C系统的容错设计基石

要理解对称性破缺技术的用武之地，首先得摸清核电站I&C系统的“脾气”。这类系统的设计遵循着严格的纵深防御原则。简单类比，就像一座城堡有多道城墙，一道被攻破，后面还有防线。在I&C架构中，这体现为多个独立的安全层级（DiD Levels），例如预防异常运行、控制异常运行、缓解事故后果等。每个层级内部，关键的安全功能往往通过硬件冗余来实现——同一个功能由多个完全相同的硬件通道（称为“分区”或“序列”）并行执行。例如，一个反应堆保护信号可能由4个独立的处理器通道同时计算，最终通过“少数服从多数”的表决机制输出。

这种设计带来了两个对验证至关重要的特性：冗余性和对称性。冗余性意味着存在多个功能相同的副本；对称性则意味着这些副本不仅在内部逻辑上相同，其与系统其他部分的连接模式也遵循某种规律（如全连接、环状连接）。正是这种对称性，为我们进行验证优化提供了突破口。

2.2 模型检验的挑战与对称性带来的机遇

模型检验的基本流程是：首先，将待验证的系统（包括其软件逻辑和硬件拓扑）抽象为一个形式化模型，通常是一个有限状态迁移系统。然后，用时态逻辑公式精确描述需要验证的属性，例如“任何情况下，紧急停堆信号最终都能被正确触发”（LTL属性：G F trip_signal）。检验器会遍历模型的所有可能状态和迁移路径，检查该属性是否始终成立。

在核电站I&C系统的模型中，故障注入是验证容错能力的关键环节。我们需要模拟各种硬件故障，如传感器失效、处理器宕机、通信中断等，并检查系统在部分组件失效后，安全功能是否依然得以保持。对于一个具有N个冗余通道的系统，考虑单故障准则（任何单点故障不导致功能丧失），理论上需要验证N种不同的单故障场景。如果考虑共因故障（CCF，多个通道因同一原因同时失效），组合数量会更多。这就是计算复杂度的主要来源。

然而，由于系统的对称性，许多故障场景在逻辑上是等价的。例如，在一个4冗余的对称子系统中，假设我们关注通道A的输出，那么“通道1故障，验证通道A”与“通道2故障，验证通道A”这两个场景，如果通道1和2在系统拓扑中地位完全对称，其验证结果应该是相同的。如果我们能自动、严谨地证明这种等价关系，就可以只验证其中一个场景，从而将验证工作量减少近一半甚至更多。这就是对称性破缺的核心思想：通过形式化推理，识别并消除由系统对称性产生的、验证意义上的冗余场景。

2.3 形式化定义：配置、支配关系与等价类

为了自动化这个过程，研究团队建立了一套严谨的数学框架。首先，他们将一个待验证的具体场景定义为一个验证配置，记作c = (u, i, φ)。这里：

• u是视点单元，即我们关心其输出行为的那个逻辑模块（例如，某个安全功能的最终表决器）。
• i是该单元的视点分区，即我们具体观察该单元的哪个冗余副本。
• φ是故障分配，一个函数，精确指定了系统中哪些单元的哪些分区被注入了故障。

基于此，他们定义了配置之间的支配关系。如果配置c1支配c2（记作c1 ≥ c2），那么意味着在c1所描述的故障环境下，系统行为集合包含了c2环境下的所有可能行为。换句话说，c1的故障假设比c2“更严苛”或“更不乐观”。由此可以得出一个关键推论：如果一个安全属性在更严苛的配置c1下被验证为真，那么它在被支配的、相对宽松的配置c2下也必然为真。

如果两个配置互相支配，则它们构成等价关系。所有等价的配置可以归为一个等价类，每个等价类中只需任选一个代表进行验证即可。自动化对称性破缺算法的目标，就是通过分析系统的模块连接图、单元分组和对称性声明，自动计算出所有待验证配置之间的支配与等价关系，最终筛选出一个最小且充分的验证配置集合。

注意：这里的“行为集合包含”关系是定义支配关系的基石。对于线性时态逻辑（LTL）属性，由于其语义是“在所有行为路径上都成立”，该推论直接有效。但对于计算树逻辑（CTL）中的某些属性（如AG EF p，表示在任何可达状态下属性p都可能为真），情况更为复杂，需要特殊的故障建模处理，下文会详细展开。

3. 方法论实现：自动化对称性破缺的技术拆解

3.1 系统建模与对称性声明

自动化分析的前提是有一个机器可读的、富含结构信息的形式化模型。研究团队使用的工具链（HW-SW-builder）允许用户以文本或图形化方式，基于预定义的基本功能块库来构建I&C系统模型。关键的一步是，用户需要在模型中显式声明单元组和对称性。

• 单元组：将系统中所有完全相同的冗余模块归类到一个组内。例如，一个4冗余的保护系统（PS）的四个处理通道可以定义为一个单元组g_ps，其分区数d(g_ps) = 4。
• 对称性声明：在模块接口层面，声明哪些输入变量组是对称的。例如，一个表决器模块可能有四个输入in1, in2, in3, in4，分别来自四个冗余通道。如果该表决器是对这四个输入进行“三取二”或“四取二”逻辑运算，那么这四个输入在逻辑上就是完全对称的——任意交换它们的连接，模块的输出行为不变。这个信息需要由设计者或验证工程师根据设计意图提供，但工具可以辅助进行一致性检查。

模型在内部被表示为一个有向无环图（DAG），顶点是模块、变量等组件，边代表信号连接。这种表示便于进行上游/下游的依赖关系分析，这是递归判断支配关系的基础。

3.2 支配关系的递归判定算法

判断两个验证配置c1和c2的支配关系，本质上是在比较从“视点”模块出发，逆向回溯到系统输入的这一条信号链路上，故障影响的严重程度。

算法采用递归下降的策略，从视点模块开始，比较其自身及上游组件的故障状态：

1. 基础情况（输入变量）：如果比较的两个组件是系统输入变量，则它们是否可比取决于是否属于同一系统输入组。支配关系则直接比较其故障状态（是否被注入故障）。
2. 递归步骤（模块）：如果要比较两个模块M1和M2，算法首先检查它们是否属于同一单元组（即可比）。然后，递归地比较它们的所有输入。这里的关键是处理对称输入组：如果模块声明了某些输入是对称的，那么算法需要尝试寻找这些对称输入之间的一个匹配排列，使得在某种排列下，M1的每个输入都支配M2的对应输入。这涉及到对对称组内元素进行排列组合的搜索。
3. 故障状态比较：在递归比较的每一步，都会综合考量组件自身的直接故障假设（φ）以及从其上游传递下来的故障影响。规则是：如果一个组件处于故障状态（其输出可能被任意值替代），那么它所能产生的行为集合是最大的（即最不确定的），因此它支配任何在相同位置没有故障或故障更少的对应组件。

该算法通过Prolog逻辑编程语言实现，利用其强大的逻辑推理和搜索能力，可以高效地处理对称组内的排列匹配问题。在实际案例中，尽管对称组大小可能达到4，但整个分析过程通常在1秒内即可完成，开销几乎可以忽略不计。

3.3 针对不同时态逻辑属性的适配处理

并非所有验证属性都能直接从支配关系中受益。研究团队将属性分为几个类别，并采取了不同的策略：

• 通用LTL属性：这是最直接的情况。由于LTL属性要求在所有行为路径上成立，而更严苛的故障配置（c1）会产生更多（或至少相同）的行为路径，因此，如果在c1下属性成立，在被c1支配的c2下也必然成立。对称性破缺可以直接应用。
• 孤立LTL属性：这类属性只涉及视点单元自身的变量，不涉及上游受故障影响的信号。因此，故障配置对其无影响，所有故障场景下的验证都是等价的，只需任选一个配置验证即可。
• 全局可能性属性（AG EF f）：这是CTL属性中的一个重要子类，用于表达“在任何可达状态下，总存在一条未来路径使得条件f成立”。这种属性对故障建模非常敏感。一个反直觉的情况是：向系统中添加故障（使行为更不确定）有时反而会破坏这种“可能性”属性，因为故障可能引入一些新的、糟糕的状态，从这些状态出发，原本可达的好状态变得不可达了。

为了解决这个问题，使对称性破缺对这类属性依然有效，论文提出了一种精化的故障注入方法。他们为模型引入了一个全局的“故障使能”比特位γ。该比特位在初始时非确定性地为0或1，并且只能从1变为0，不能从0变回1。故障模块只有在γ=1时才真正生效，替代信号值。这种设计创造了一种“故障可能发生，但最终会停止”的语义。可以证明，在这种精化故障模型下，如果AG EF f在更严苛的配置c1下不成立（即存在一个状态，从那里f永远不可达），那么在c1支配的c2下，该属性也必然不成立。这使得支配关系推理得以延续。当然，这种精化会增加模型的状态空间，因此仅在对AG EF类属性进行验证时启用。

4. 案例研究：方法在虚构核电站I&C模型中的实践

4.1 案例系统架构与功能

为了验证方法的有效性，研究团队构建了一个基于美国EPR核电站设计理念的虚构案例。该系统包含多个遵循纵深防御原则的容错子系统，结构比先前的研究更为复杂：

1. 过程自动化系统（PAS）：负责电厂正常运行（非安全功能），只有1个分区。它根据冷却能力计算允许功率，并通过PID控制器控制棒位。
2. 保护系统（PS）：4冗余的安全系统，属于纵深防御第3级，与PACS共同执行反应堆保护功能。需满足单故障准则（同一分区内PS和PACS同时故障被视为一个 consequential failure）。
3. 安全自动化系统（SAS）：2冗余的安全系统，属于纵深防御第2级，与PACS共同执行预防性保护功能。需满足单故障准则（仅SAS或仅PACS单故障）。
4. 优先级与执行器控制系统（PACS）：4冗余系统，同时参与第2级和第3级安全功能。

这些子系统之间存在着复杂的交叉连接，模拟了现实中难以完全实现各防御层级绝对独立的情况。每个子系统内部又由采集处理单元（APU）和动作逻辑单元（ALU）等模块构成，通过全连接等方式交互。

4.2 验证场景与故障准则配置

根据纵深防御原则和功能分配，设定了不同的验证场景和对应的故障容忍准则：

• 场景1（Level 1 - 正常运行）：验证PAS功能。假设其上游的PS无故障。
• 场景2（Level 2 - 预防性保护）：验证SAS和PACS的共同功能。要求容忍SAS或PACS中的单故障，以及PAS的共因故障。在实际验证中，可简化为仅考虑SAS单故障（因为从视点分析，PACS的视点不受SAS故障影响，反之亦然）。
• 场景3（Level 3 - 反应堆保护）：验证PS和PACS的共同功能。要求容忍PS和PACS同一分区内的共模单故障，以及SAS和/或PAS的共因故障。
• 场景4（人工场景）：不考虑DiD层级，对所有子系统独立应用单故障准则。此场景用于与先前工作对比。

对于每个场景和每个选定的“视点”单元（即需要验证其属性的具体模块），工具会自动生成所有可能的验证配置组合（视点分区 × 故障分配）。

4.3 对称性分析结果与验证效率提升

应用自动化对称性破缺算法后，得到了清晰的支配关系矩阵。以某个复杂场景为例，原始需要验证的配置数量可能是16个。通过分析，工具识别出其中存在一个“顶级”配置，它支配了所有其他配置。同时，还存在多个等价类。

结果：工具自动筛选后，实际需要执行模型检验的配置数量大幅减少。在论文展示的案例中，验证效率最高提升了24倍（与暴力验证所有可能配置的“朴素方法”相比）。这个提升倍数直接对应于被剪枝掉的冗余配置的比例。对称性分析本身的计算耗时极短（不足1秒），远少于运行一次模型检验所需的时间（可能从数秒到数分钟不等）。这意味着，该方法以几乎可忽略的预处理开销，换来了验证任务数量一个数量级的减少，对于需要反复验证大量属性的工程实践而言，价值巨大。

实操心得：在实际工程中应用此方法时，关键在于准确地进行系统建模和对称性声明。工程师需要仔细梳理系统设计文档，明确所有冗余单元的分组，并判断模块输入端口之间的对称关系。一个常见的误区是，仅因为硬件模块相同就认为其输入对称，而忽略了连接拓扑可能引入的不对称性（例如，某个通道的输入来自特定的传感器组）。错误的对称性声明会导致工具推导出错误的支配关系，进而可能漏掉关键的故障场景，造成验证不完整。因此，建议在声明对称性后，先用工具对一个小规模属性进行验证，对比启用和禁用对称性破缺的结果，以确保对称性假设的正确性。

5. 工程实践指南：应用对称性破缺的要点与避坑

5.1 工具链集成与工作流

将自动化对称性破缺集成到现有的I&C系统形式化验证流程中，可以遵循以下步骤：

1. 系统形式化建模：使用支持模块化、层次化建模的工具（如论文中的HW-SW-builder或其等效工具），将I&C系统的功能块图（FBD）转换为形式化模型。务必在模型中显式标注单元组（unit groups）和模块的输入对称性（input symmetries）。
2. 属性规约编写：用时态逻辑（LTL或CTL）编写需要验证的安全属性。注意属性的类别（通用LTL、孤立LTL、全局可能性CTL），这会影响后续故障模型的选用。
3. 验证任务定义：指定验证场景（对应哪些DiD层级和故障准则）以及“视点”单元。工具会根据这些信息，自动生成完整的验证配置集合。
4. 运行对称性分析：调用对称性破缺引擎（如集成的Prolog推理模块）。引擎会读取模型、属性和验证任务，计算配置间的支配/等价关系，并输出一个最小化的、待验证的配置列表。
5. 执行模型检验：对筛选后的配置列表，逐个调用后端模型检验器（如nuXmv）进行验证。可以并行执行以加快速度。
6. 结果分析与迭代：分析验证结果（通过或反例）。如果发现反例，需要根据反例路径调试系统设计或模型。由于对称性破缺保证了验证的完备性（在给定的对称性假设下），一个配置上的反例足以揭示一类对称配置下的缺陷。

5.2 适用范围与局限性

该方法并非万能，清楚其边界至关重要：

• 支持的属性类型：方法主要适用于那些关注单个“视点”单元及其上游组件行为的属性。对于需要考察多个非上下游关系的单元间协同行为的属性（例如，“模块A和模块B的输出永远不会同时为高”），当前的支配关系推理框架不适用。
• 对内部变量的访问：如果属性需要查询可能受故障影响的模块的内部变量（而非仅输出），则需要通过技术手段将这些内部变量“连线”到额外的输出端口，否则故障注入可能无法正确影响这些变量。
• 模型结构限制：当前方法要求整个系统的模块间连接图是无环的。虽然许多I&C系统的数据流是前向的，但某些设计（如包含周期性自检的反馈回路）可能引入环。论文指出，通过考虑有限长度行为上的包含关系，理论上可以支持环，但这需要更复杂的归纳证明，是未来的研究方向。
• 异步与通信延迟：当前工作未显式处理模块间的异步执行和通信延迟。虽然可以通过在连接中插入延迟模块来建模，但这会显著增加验证复杂度，通常需要借助有界模型检验（BMC）等技术。

5.3 常见问题与排查技巧

在实际应用过程中，可能会遇到以下典型问题及解决思路：

1. 问题：对称性分析时间过长。

   • 排查：检查模型中声明的对称组大小。如果对称组包含的元素非常多（例如超过10个），排列组合的搜索会变得非常耗时。这通常意味着模型抽象层次过高，或者对称性声明过于笼统。
   • 解决：尝试细化模型，将大模块拆分为更小的子模块，从而减少单个对称组的规模。或者，重新评估对称性声明的准确性，看是否某些输入实际上并不完全对称。

2. 问题：模型检验在某个配置下超时或内存溢出，而该配置是筛选后必须验证的。

   • 排查：这通常是模型本身状态空间过大导致的，与对称性破缺无关。检查该配置是否引入了最复杂的故障组合（例如，多个单元的共因故障）。
   • 解决：可以尝试启用模型检验器的更多优化选项，如COI（锥形影响）约减、对称性约减（这里是模型检验器自身的，而非我们前期的）、BMC（有界模型检验）等。如果问题依旧，可能需要考虑对模型进行进一步的抽象，例如合并一些内部状态，或者采用分层验证的策略。

3. 问题：验证通过，但对结果的信心不足，担心对称性声明有误。

   • 排查：这是对形式化方法常见的“验证的验证”问题。
   • 解决：可以采用交叉验证。首先，在不启用对称性破缺的情况下，随机选择少量（非最小集）配置进行验证，结果应与启用对称性破缺后其代表配置的结果一致。其次，可以进行“负测试”：故意修改设计，引入一个已知的、不对称的缺陷，然后看对称性破缺后的验证是否能发现它。最后，将对称性声明作为重要的设计文档进行同行评审，确保其与系统设计意图一致。

4. 问题：对于AG EF类属性，精化故障模型下验证时间显著增加。

   • 排查：引入全局故障使能比特γ确实会扩大状态空间，因为系统需要记录故障是否已被“冻结”。
   • 解决：评估是否必须验证此类属性。有时，可以用更强的LTL属性（如G (p -> F q)）来替代部分AG EF的需求。如果必须验证，可以尝试调整模型检验器的搜索策略，或设定更长的超时时间。同时，确保只在对AG EF属性验证时才启用精化故障模型，对LTL属性则使用普通故障模型。

将对称性破缺技术整合到核电站I&C系统的形式化验证流程中，标志着我们从依赖专家经验的手动优化，走向了基于形式化推理的自动化、可重复的验证效率提升。这项工作的价值不仅在于其算法本身，更在于它提供了一套完整的、可工程化的框架，让复杂系统验证中的“组合爆炸”问题变得可控。它提醒我们，在面对极度复杂的系统时，巧妙利用系统自身的设计特性（如为容错而生的对称性），往往是破解验证难题的关键。