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

唐瑞泽 等: 分布式系统模型检验技术研究进展 2181

从以上研究可以看出, 可靠型通用分布式系统状态空间约减技术已被广泛研究, 许多工作的核心贡献即在于
提出或优化状态约减算法. 然而, 尽管这些约减技术在理论上是正交的, 它们的结合并不容易. 目前尚未有 DMCK
研究同时集成所有这些约减算法.
不可靠型 (unsound) 约减方法: 不可靠约减方法通常利用领域知识或启发式策略, 针对特定场景进行优化, 例
如启发式丢弃状态、存储状态时忽略部分变量、限制探索深度等.
CMC [42] 采用启发式算法标记某些状态为更有价值的状态, 使其优先被探索, 而价值较低的状态可能被丢弃.
该启发式算法倾向于搜索明显偏离常规的状态, 其核心思想是: 如果状态的比特位数突然增加, 或变量取值变得罕
见, 则认为该状态更有价值. 此外, CMC 允许在状态标准化时剔除用户认为不重要的内存信息, 使得某些状态被视
为等价.
MoDist [49] 结合多种策略来有效发现缺陷, 例如使用随机策略发现浅层缺陷, 并结合随机探索与 DPOR 提高路
径多样性. 由于随机策略的引入, 部分状态可能无法被探索. DeMeter [40] 采用快照机制, 对感兴趣的状态进行存储,
并将这些状态作为初始状态进行探索, 同时丢弃不感兴趣的状态, 导致约减方法不可靠.
MaceMC [45] 旨在发现活性 (liveness) 属性被违反的缺陷, 采用三阶段状态探索方法来检查活性属性. 其中, 前
两个阶段使用有界深度优先搜索 (bounded depth-first search, BDFS) 探索状态空间到一定深度, 并利用随机游走策
略深入探索可能导致活性属性违反的外围状态. 对于超过上万深度的随机游走仍无法满足活性属性的路径, MaceMC
启发式地标记其为违反路径. 这种限定深度和随机游走策略使得 MaceMC 的约减方法不可靠.
CrystalBall [50] 主要针对已部署分布式系统的在线模型检验, 旨在预测和预防系统进入不一致状态. 由于分布式
环境难以获取全局一致性快照, CrystalBall 仅对节点及其通信的邻居节点进行局部快照和模型检验, 采用迭代加
深的深度优先搜索算法, 并根据设定的时间约束停止搜索. CrystalBall 属于不可靠型约减, 因为其模型检验仅针对
特定时机进行空间和时间上的限定, 尽管能聚焦最关心的状态, 但无法捕捉整个分布式系统的全局状态变化可能
带来的缺陷. 此外, 搜索时间受限可能导致未能探索到导致缺陷的深度.
CrystalBall 的后续工作 LMC [57] 也面向在线模型检验, 提出了与 DeMeter 类似的观察, 即全局状态由所有节点
状态和网络状态组成, 并且二者是可以分离的. 不同的是, LMC 观察到网络状态的频繁变化会导致大量不同的全
局状态, 使得在线模型检验难以在短时间内达到有意义的深度. LMC 进一步发现网络状态并不用于属性检查, 因
此提出“局部模型检验 (local model checking, LMC)” 技术, 该技术使用共享的网络状态, 包含网络中所有历史消息
(即发送到网络的消息不会被删除), 仅根据节点状态区分状态是否相同, 并将共享网络状态与节点状态合成全局
状态进行检验. 这种方法可能导致系统进入实际不存在的状态, 因此 LMC 在检测到属性违反后, 会对执行路径进
行检查, 确保报告的反例真实存在. 由于该方法面向已部署系统的在线检验, 相较于传统探索方式, 它能在数秒内
探索到一定深度 (如 20–30 层状态), 当网络消息过多导致状态爆炸时, LMC 关注的是系统运行中的最新状态, 而
不会处理所有可能的状态.
从以上不可靠型约减方法的研究可以看出, 传统 DMCK 工具大多采用不可靠型约减来加速缺陷发现. 这反映
出状态爆炸问题的严峻性, 使得通用型可靠状态约减技术已接近瓶颈, 促使这些工具在牺牲可靠性的前提下换取
更高效的缺陷发现能力.
3.2.3 状态探索效率优化
与状态空间约减正交的缓解状态爆炸问题的方式是优化探索速度. 探索速度越快, 有限时间内能够探索的状
态或路径数量就越多. 一些工作在单个模型检验进程内模拟分布式系统节点和环境 [42,45,52] . 尽管这种方式通常状
态探索速度较快, 但它仅适用于使用特定框架编写的程序, 或者需要较高的适配成本. 越来越多的工作则在更真实
环境中启动多个分布式系统节点 [11,40,49,67,71,73] , 这些工作通常基于无状态搜索技术. SandTable [71] 总结了 3 大原因,
导致传统 DMCK 状态探索速度较慢: 1) 无状态搜索回溯时重复执行事件序列 (例如反复重新初始化); 2) 代码事件
执行速度较慢 (例如文件 I/O); 3) 模型检验代码带来的额外开销 (例如事件调度同步开销). 相关工作的优化策略通
常有一定共性, 主要通过虚拟时钟、缓存部分状态 (尤其是初始状态) 和减少事件执行间等待时间等手段来提高