Page 307 - 《软件学报》2026年第5期

2186 软件学报 2026 年第 37 卷第 5 期

SAMC 通过恢复抽象全局状态 (recovery abstract global state, RAGS) 来实现这一优化, 其中, 抽象状态表示只包
含部分变量的状态子集. 首先, 如果两个恢复动作产生相同的消息, 并以相同方式改变恢复抽象局部状态 (recovery
abstract local state, RALS), 则它们被视为对称的. 随后, SAMC 分析恢复相关代码, 并计算不同节点在该崩溃事件
下的恢复代码如何影响 RALS 及可能发送的网络消息. 然后, 所有 RALS 经过排序后合并, 形成 RAGS. 最终, 在注
入崩溃事件前, 若某个恢复抽象全局状态已出现过, 则该崩溃事件不再被注入. 本质上, SAMC 的崩溃恢复对称性
处理方式与有状态搜索中的状态标准化 (state canonicalization) 类似或部分实现了这一过程. 通过对恢复抽象局部
状态的排序和合并, 消除了节点 ID 的影响, 相当于在等价错误注入中选取一个代表, 并将该抽象状态用于对称性
约减中的状态去重. 用户需建模各节点的 RALS 变量及其在崩溃恢复事件中的更新方式, 以使用该约减策略.
FlyMC 进一步泛化了对称性, 涵盖通信对称性和状态对称性. 分布式系统中的节点通常具有相同角色 (例如
跟随者), 且其状态转移仅取决于接收消息的内容, 而与发送或接收节点的 ID 无关. FlyMC 通过记录抽象状态-事
件转移历史来识别对称性. 其中, 抽象状态去除了与节点 ID 相关的信息, 并对各节点的状态进行排序后合并. 后续
状态空间探索时, 若遇到相同的抽象状态-事件转移, 则表明该执行路径已被探索, 从而避免冗余计算. 本质上,
FlyMC 的方法与 SAMC 类似, 都借鉴了有状态搜索中的对称性处理方式, 以减少等价状态遍历.
MP-Basset [59] 的后续工作 DBSS (decomposition-based stateful search) [60] 采用状态分解 (state decomposition) 方
法, 将协议状态划分为相关变量 (relevant) 和辅助变量 (auxiliary). 其中, 相关变量影响协议行为, 而辅助变量不会
影响协议行为. 在状态去重过程中, 仅考虑相关变量. 在计算状态哈希前, DBSS 通过状态标准化选择对称状态中
的代表性状态进行存储和去重. 该方法要求被忽略的辅助变量不会影响未来状态转移, 而这取决于系统本身及待
检查的属性, 因此需要具有系统领域知识或语义信息的专家进行分解. DBSS 相比传统方法约减了高达 39% 的状
态空间, 但该工作主要侧重于算法的可靠性 (soundness) 证明, 尚未在大规模分布式系统的模型检验中广泛应用.
4.2.3 垂直领域约减
对于完整的分布式系统状态空间, 模型检验难以穷尽所有路径. 垂直领域约减聚焦于特定系统行为或故障
模式 (如错误注入、容错逻辑等), 结合领域特定的语义信息, 剪裁与目标属性无关的状态空间, 从而显著提升验
证效率. 这类语义信息通常来源于对垂直领域的专门建模过程, 本质上将领域知识直接编码进模型中, 使状态空
间探索更具针对性. 例如, SAMC、FlyMC 和 MP-Basset 利用容错逻辑、错误注入和协议级语义, 在人工建模中
主动排除了与验证目标无关的状态空间, 主要包括某些局部事件引起的线程调度交织, 从而聚焦于垂直领域相
关的关键行为.
此外, 一些研究借鉴模型检验的基本原理, 聚焦于特定垂直领域, 通过引入领域特定的语义信息, 仅探索与该
领域相关的状态, 或仅检测特定属性的违反, 从而有效剪裁与验证目标无关的状态空间, 提升缺陷发现效率或正确
性保障能力. 例如, 错误注入已成为分布式系统中一个典型的垂直领域研究方向. 尽管此类工作通常不属于严格意
义上的 DMCK (例如不支持确定性模拟执行), 但在垂直领域约减下依然具有重要的实践价值. 下面将简要介绍几
项具有代表性的研究.
FATE/DESTINI [107] 借鉴模型检验的穷举搜索思想, 系统性探索故障序列 (FATE) 并使用 Datalog 规约
(DESTINI) 检查正确性. FATE 通过 failure ID 抽象错误场景, 结合静态信息 (源文件、调用)、动态信息 (调用栈、
节点 ID) 以及领域相关信息 (消息类型等). 由于暴力枚举带来的状态爆炸问题, FATE 利用领域信息优先探索更可
能增加覆盖率的故障序列来优化搜索. DESTINI 采用 Datalog 语言, 解决了如何精确定义期望行为以辅助恢复代
码测试的问题. FATE/DESTINI 在 HDFS 等工业系统中发现了 16 个新缺陷, 并复现了 51 个已知缺陷. 不同于
FATE 的正向搜索策略, Molly [108] 采用 LDFI (lineage-driven fault injection), 从正确执行结果反向推导关键故障点,
逐步加深注入层级, 以减少错误注入次数, 并保持类似于模型检验的覆盖完整度. LDFI 基于 Dedalus 语言高效提
取数据谱系, 结合 SAT 求解器快速识别潜在错误组合, 避免冗余探索. Modulo [109] 关注分布式系统状态收敛性, 提
出基于模型的测试方法, 发现收敛失败缺陷 (convergence failure bug, CFB). 与 DMCK 逐步操控每个不确定性事件
的方式不同, Modulo 通过构建发散-收敛模型减少状态空间. 其方法由抽象执行模型 (AEM) 和具体执行模型 (CEM)