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

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

型层, 代码层则通过确定性模拟执行进行重放, 以支持一致性比对和缺陷确认. 在一致性比对阶段, 模型与代码的
互动主要依赖两类技术: 自顶向下 (第 5.2.1 节) 和自底向上 (第 5.2.2 节). 理论上, 这两类技术均可支持高层次和低
层次规约的互动, 但在实践中, 由于高层次规约与代码实现差距较大, 自顶向下技术的互动效果往往不理想. 已有
工作多采用低层次规约 (如 SandTable 与 Remix). 而在处理高层次规约时, 自底向上技术通常会放宽条件, 转而采
用轨迹确认技术 (第 6.2 节).
低层次规约完成一致性比对后, 规约达到较高质量, 探索状态空间的代价得以从代码层卸载到模型层. 模型层
可直接借助成熟的规约级模型检验工具, 这些工具通常集成了高效的状态约减技术 (如状态去重、对称约减、偏
序约减等), 且避免了直接运行代码的高成本, 实现更快速的缺陷发现. 例如, SandTable 实验表明规约层探索状态
空间的速度相较代码层提升了 114–2 989 倍.
在模型层发现缺陷后, 相关技术通常进一步在代码层重放缺陷事件序列, 确保缺陷能准确复现, 以便于理解、
调试和修复. 这一过程中, 确定性模拟执行 (第 3.1 节) 技术再次发挥关键作用, 实现了模型与代码之间的精准
互动.

6 分布式系统模型检验派生技术

一些方法使用了部分 DMCK 关键思想, 在不同环节进行适当改进后, 形成了一些更适用于特定场景的变体方
法. 我们将这类方法统称为 DMCK 的派生技术. 主要包括两类: 一是模型检验驱动的分布式系统测试 (model-
checking-driven testing), 二是分布式系统的轨迹确认技术 (trace validation).
6.1 模型检验驱动的分布式系统测试
测试技术因其高效性和实用性, 在分布式系统中被广泛用于缺陷发现. 许多工作采用随机、覆盖率反馈等方
式运行系统并注入故障, 如 Jepsen [15] 、Chaos [16] 、CrashFuzz [17] 等. 这些方法无需对分布式系统的执行进行确定性
控制, 也不依赖穷尽式的状态空间探索, 因此实现成本较低. 然而, 它们通常面临缺少正确性判据 (oracle) 的问题,
且在发现深层次边缘缺陷、复现缺陷和提供正确性保障方面存在不足.
为了进一步发现深层次复杂缺陷, 必须生成高质量的测试用例, 而这往往是测试技术中的瓶颈. 由于规约技术
已成为验证分布式系统核心协议正确性的主流手段, 直接复用模型检验过程中的状态空间信息, 生成高覆盖率、
高质量的测试用例, 是一种性价比极高的方案. 由于分布式系统的不确定性, 模型检验驱动的测试方法通常需配合
确定性模拟执行技术, 以保证生成的测试用例在真实系统中复现, 这种方式类似于自顶向下的一致性比对技术.
MET (model-checking-driven explorative testing) [138] 通过模型检验验证了其设计的新的 CRDT 协议的正确性,
并将模型检验结果用于指导测试. 该工作基于 Redis 实现了设计的 CRDT 协议, MET 手动插桩了 Redis 系统, 使得
客户端操作、消息传递、网络错误等事件被确定性模拟操控执行, 从而驱动测试用例的执行. 这种方法不仅在规
约层确保设计正确的基础上, 也大幅提升了对实现正确性的信心.
Mocket (model checking guided testing) [82] 要求用户提供高层次、已验证的 TLA+ 规约, 使用模型检验工具探
索状态空间并保存状态空间图, 再通过图遍历算法生成测试用例. Mocket 利用 ASM 字节码插桩技术支持对分布
式系统的确定性模拟执行, 并对执行结果进行一致性检查, 不一致即意味着潜在缺陷. Mocket 应用于 ZooKeeper
和多个 Raft 系统中, 其中 Raft 系统直接使用了 Raft 作者提供的高层次规约. Mocket 成功发现或复现了 9 个难以
通过随机测试发现的缺陷. 然而, 已有的或自行编写的高层次规约并不总是高质量的, 不一致可能来自规约自身问
题、代码实现与规约设计偏离等. 因此 Mocket 发现不一致后, 仍需人工分析是误报、代码缺陷还是规约错误. 其
实验结果表明, 3 类情况均有发生.
6.2 分布式系统轨迹确认技术
自底向上的一致性比对技术虽理论完备 (第 5.2.2 节), 但在实际应用中成本极高而不切实际. 后续研究发展出
分布式系统轨迹确认技术 (trace validation), 通过放弃穷举探索或放宽轨迹与状态空间的匹配条件, 大幅提升了其
实用性和有效性.