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

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

这一方法最早由文献 [135,136] 描述, 类似于构建精化关系 (refinement) [134] . 但这些相关研究的研究重点不在
轨迹生成策略上, 通常简单地采用随机等策略来生成执行轨迹. 该技术在分布式系统中的首次应用是在 MongoDB
中, 并被称为 MBTC (model-based trace checking) [127] . MBTC 中的代码执行轨迹通过现有的集成测试和随机测试生
成, 而规约则复用了 MongoDB 设计的基于拉取的 Raft 改进版协议 TLA+ 高层次规约. MBTC 的验证过程使用了
TLA+ 传统的精化映射方法, 以验证代码执行轨迹是否符合高层次规约的精化关系.
然而, MongoDB 团队发现 MBTC 实施效果不佳. 尽管投入了大量的人力和时间, 最终并未达到预期效果. 在
此过程中, 有大量的模型与代码不一致的情况, 但这些不一致经过人工分析后并非代码缺陷, 反而需要通过避免产
生不一致的执行轨迹、修改规约或强行模拟一致等方式来解决问题. 最终, 5 个测试中只有一个通过了 MBTC 的
一致性比对. 开发者意识到, 规约必须与代码更加接近才能让这种技术更具实用性. 尽管 MongoDB 团队随后重新
编写了更贴近代码的 Raft 规约, MBTC 仍未成功实施. 这主要因为精化关系验证过于严格, 要求每条轨迹中包含
规约中的全部变量, 而实际中很难完整获取所有变量. 同时, TLC 工具当时缺乏对轨迹验证的关键支持.
后续研究通过放宽轨迹与状态空间的匹配条件, 大幅提升了其实用性和有效性. 该方法的核心思想是, 执行轨
迹只需提供部分变量状态, 由模型检验工具自动推导缺失变量, 从而构造一个状态空间. 只要该状态空间与规约的
状态空间存在交集, 即认为该轨迹与规约一致.
SEFM [137] 工作基于 TLA+ 提出了自动推导缺失变量的轨迹确认框架, 框架支持从分布式系统收集日志并在
TLC 工具中验证轨迹与规约的一致性. 该流程首先对被测系统进行随机执行 (例如使用被测系统的端到端测试套
件等, 不需要确定性模拟执行技术), 随机执行过程中可随机注入节点故障和网络错误. 然后收集各节点日志, 日志
需记录关键事件名与部分变量信息. 随后, 分布式系统各个节点的所有事件按时间戳 (或逻辑时钟) 全局排序, 生成
一条串行执行路径. 轨迹确认阶段中, 该路径被输入 TLC 工具, 每个事件和变量赋值被编码到规约的状态转移使能
条件中, 从而将状态空间限制在当前轨迹事件允许的状态范围内 (轨迹中记录的变量越多, 则限制的状态空间越精
确). 若 TLC 探索的状态抵达轨迹末尾的事件, 则视为轨迹与规约一致; 若提前终止状态探索, 则表明存在不一致.
SEFM 所提出的轨迹确认技术已在微软 CCF 项目 [122] 和开源 etcd [123] 中取得成功. 在 CCF 中, 该技术被称为
Smart Casual Verification, 即介于严格和不严格之间的轻量级验证技术. 开发者为共识模块和客户端一致性模块编
写了高层次 TLA+ 规约, 并复用原有测试生成日志用于验证. 尽管日志中不包含全部变量的赋值, TLC 工具依然
能根据规约和轨迹使能条件限制有效推导缺失变量的可能状态. 根据我们的观察, 轨迹确认还缓解了规约与代码
粒度不一致问题, 可通过对规约的动作合并和对轨迹的事件筛选来对齐二者粒度, 使得高层次和低层次规约均可
用于真实代码的比对. CCF 团队通过模型检验和基于 Q-Learning 的模拟测试 (simulation testing) 等方式, 发现了 6
个缺陷. 尽管轨迹确认技术无法自动复现这些缺陷, 但缺陷可通过已有测试或手动复现方式确认.
总体而言, 轨迹确认技术作为互动式 DMCK 的实用化变体, 有效利用了模型层的状态探索能力, 又避免了代
码层确定性控制的高成本. 其在 TLA+ 工具链中已逐渐发展成熟, 并因其易用性和粒度对齐的灵活性, 在工业界逐
渐获得认可和采用.
7 总结和展望

分布式系统作为现代计算基础设施的核心, 其可靠性与正确性至关重要. 然而, 由于运行环境的不确定性以及
代码设计与实现的高度复杂性, 验证其正确性始终是一项极具挑战的任务. 分布式系统模型检验 (DMCK) 通过穷
尽式状态探索, 有效应对了不确定性所带来的“缺陷难发现、难诊断、难修复”等难题. 本文梳理了 DMCK 的关键
研究进展, 归纳为 3 个阶段, 并在此基础上分析当前存在的局限与未来发展方向.
7.1 分布式系统模型检验工作的总结
分布式系统模型检验技术在早期缓解了建模成本高和模型与代码存在语义鸿沟的问题, 但也带来了严重的状
态爆炸挑战. 通用状态约减方法逐渐达到瓶颈, 引入适量人工的系统特定语义优化成为有效补充, 显著缓解了该问
题. 随后, 形式化规约的引入以及规约与代码互动技术的推进, 进一步提升了 DMCK 效率与可用性. 在这一演进过