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

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

(distributed system model checking, DMCK) 是在软件模型检验 (software model checking) [27] 基础上发展而来的一个
子方向, 该术语最早由 SAMC [11] 提出, 专注于验证分布式系统的真实代码. 它结合了两个关键要素: 代码级模型检
验和面向分布式系统的针对性适配.
首先, 代码级模型检验在系统的真实代码上进行状态空间探索, 而非仅对系统的抽象模型进行验证. 这一方式解
决了传统模型检验中模型与代码之间存在的语义鸿沟问题, 能够更有效地发现实际系统中的缺陷, 且验证结果直接
反映到代码. 然而, 它仍面临如何在代码层控制分布式系统固有的不确定性, 以系统性覆盖所有可能执行路径的挑战.
其次, 分布式系统特有的不确定性进一步加剧了代码级模型检验中的状态爆炸问题, 主要体现在两个维度:
[9]
[8]
1) 系统实现的复杂性: 为满足容错需求, 分布式系统通常采用复杂的协议设计 (如 Paxos 、Raft 和 Zab [6,10] ), 并引
入多线程、磁盘异步读写、超时等实现机制, 导致状态空间极其庞大, 潜在缺陷更难被覆盖; 2) 计算环境的不确定
性: 分布式系统运行在充满异步、并发和错误事件的环境中, 例如消息延迟与乱序、节点宕机、时钟漂移、用户
请求等都可能引发大量不确定行为, 进一步加剧了状态空间爆炸问题.
因此, DMCK 在带来面向分布式系统的代码级模型检验能力的同时, 面临着如何控制环境与系统行为的不确
定性、如何缓解状态爆炸等关键挑战. 本文聚焦于真实分布式系统代码的模型检验技术, 梳理了 DMCK 从早期原
型工具到具备工业实用性的演进脉络. 在这一过程中, 研究者不断应对前述挑战, 解决了如何控制不确定性和如何
有效高效进行状态探索的问题. 通过引入系统语义信息, 降低状态爆炸程度. 通过代码层与模型层的互动, 进一步
提升了分布式系统模型检验的效率. 这些技术在保证代码级验证能力的同时, 有效提升了 DMCK 的效率与实

用性.
1.2 相关综述工作与本综述贡献

就我们前期调研的文献来看, 目前尚无专门针对 DMCK 技术的综述, 但是国内外有一些与之相关的优秀综
述. 国内研究者对形式化方法的研究进展进行了非常详尽的综述 [28] , 涵盖了形式化方法各个方面的研究现状, 但
该综述更关注于形式化验证技术本身, 而较少关注于分布式系统代码级模型检验技术. Godefroid 等人 [29] 认为模型
检验提供的保证是有限的, 在实际使用中是一种发现软件缺陷的“超级测试”, 因此也将软件模型检验称为系统性
测试 (systematic testing). 该综述主要梳理了并发系统和串行系统的相关研究, 在并发系统方面主要针对多线程并
发, 而对分布式系统的探讨较少. 国内研究者对分布式系统的动态测试技术进行了详尽的综述, 从不同类型系统缺
陷的角度介绍了典型的分布式系统动态测试工具 [30] . 其中部分 DMCK 研究被归入鲁棒性缺陷测试工具. 然而, 该
综述主要关注测试技术, 对 DMCK 相关工作的讨论较少. 国内研究者对分布式共识协议的形式化验证进行了系统
性综述 [31] , 涵盖模型检验与定理证明等方法, 但主要聚焦于协议设计层, 未涉及系统实现层的技术进展. 国内研究
者对模型检验中的状态爆炸问题进行了系统性综述 [32] , 其中总结的多种缓解技术已被广泛应用于 DMCK 相关工
作中. 此外, 国内研究者还有专门针对交互式定理证明的并发程序验证工作的综述 [33] , 详细整理了并发程序形式
化验证中定理证明方向的研究进展, 但未系统性梳理模型检验方向的进展.
我们观察到, DMCK 的发展受到传统模型检验技术演进的影响, 其核心挑战在于模型检验的效率与模型检验
的人工成本之间的权衡. 这一权衡推动了 DMCK 技术的演进. 围绕上述基本权衡, 本文梳理了 DMCK 的 3 个发展
阶段. 第 1 阶段的 DMCK 研究解决了无需人工建模即可直接检验分布式系统实现的可行性问题. 第 2 阶段为缓解
状态爆炸问题, 逐步引入被验证系统的语义知识. 近年来, 面向分布式系统协议与设计的传统模型检验技术, 在实
用性与易用性方面有了长足的进步 [34,35] . 第 3 阶段 DMCK 开始寻求与传统模型检验进行有机互动, 以进一步提升
代码级模型检验的效率. 上述发展过程形成了本文的主线.
本文第 2 节介绍综述的框架. 第 3 节描述传统 DMCK 技术, 这一阶段的核心在于实现代码层模型检验的核心
使能技术与状态爆炸缓解技术. 第 4 节介绍语义感知 DMCK 技术, 该阶段引入少量人工建模以利用系统语义信息
进一步缓解状态爆炸问题. 第 5 节讨论模型层与代码层互动的 DMCK 技术, 具体介绍分布式系统形式化建模技
术, 以及模型与代码之间的一致性比对技术. 第 6 节探讨 DMCK 派生出的新型测试和验证技术. 最后, 第 7 节对综
述进行总结并展望未来研究方向.