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

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

SCC 进行活性验证; 2) 无状态搜索从原理上无法支持 SCC 技术. 因此, 大部分 DMCK 主要关注安全性验证, 但仍
有一些工作通过启发式方法和安全性属性来近似判定活性属性 [45,49] .
MaceMC [45] 是首个主要面向活性验证的 DMCK, 认为活性与安全性同样重要. MaceMC 采用启发式方法, 检
测系统是否进入无法恢复的死状态, 而非传统活性验证要求的无穷执行路径分析. MaceMC 采用三阶段探索方法:
1) 有界深度优先搜索: 在有限深度 (约 25–30) 内穷尽所有执行路径, 识别外围状态中可能不满足活性属性的中间
状态; 2) 随机游走: 从中间状态出发, 进行深度达上万步的随机探索, 若仍未满足活性属性, 则标记为可能的活性
违反; 3) 关键转移分析: 识别导致系统进入死状态的关键转移, 以帮助开发者定位根本原因. 虽然 MaceMC 的方法
不能保证所有发现的活性违反都是实际缺陷, 但其报告的缺陷未出现误报, 表明方法有效.
MoDist 采用启发式方法结合安全性属性检查来近似验证活性: 假设在无错误注入的情况下, 系统应当持续推
进工作. 在所有被测系统中, MoDist 均发现了活性违反缺陷, 这些缺陷被确认为协议设计层面的严重问题. 值得一
提的是, MoDist 在全局一致快照中仅发现了通用安全性问题及系统自带断言的违反, 而未发现额外的领域安全性
违反. 这一结果表明被测系统的成熟度, 同时支持了 MaceMC 关于活性属性同样重要的观察.

4 系统语义感知的分布式系统模型检验

状态爆炸问题是制约模型检验可扩展性的核心挑战, 在 DMCK 中尤为突出, 其根本原因在于分布式系统设计
与实现的高度复杂性及运行环境中的高度不确定性, 导致状态空间迅速增长. 为缓解状态爆炸, 传统 DMCK 通常
基于通用策略开发了状态空间约减技术, 如状态去重、对称约减、动态偏序约减和动态接口约减等. 然而, 这些通
用约减策略缺乏对系统语义的深入挖掘与融合, 其约减能力已接近瓶颈. 为提升缺陷发现能力, 部分研究转向不可
靠约减方法 [40,42,45,49,50,57] , 虽可加速发现缺陷, 但难以提供全面的正确性保障.
为应对上述瓶颈, 研究工作开始探索如何融合系统语义信息以提升状态约减能力. SAMC [11] 指出, 传统
DMCK 未系统性利用事件间的独立性与对称性等语义特性, 导致动态偏序约减与对称约减的效果受限, 重复探索
了大量等价路径. 尤其在分布式系统中, 节点崩溃与消息传递等事件之间往往存在独立性与对称性, 但传统方法对
此缺乏建模, 从而造成不必要的状态穷举. SAMC 首次提出系统语义感知的分布式系统模型检验技术, 聚焦分布式
容错系统中普遍存在的语义特性, 开发者仅需提供少量语义建模, 即可进行高效的状态约减.
这一阶段的 DMCK 工作关注如何通过少量人工建模或标注, 显式表达系统中的对称关系、事件独立性与垂
直领域特性, 以辅助状态约减与状态划分. 实践表明, 系统语义感知的 DMCK 能显著约减状态空间, 即使不依赖不
可靠的约减策略, 仍具备高效发现深层缺陷的能力, 从而显著提升模型检验结果的有效性.
此外, 随着 DevOps (Development 与 Operations 融合的软件开发流程) 模式的普及, 开发者通常也承担测试职
责, 对系统语义具备深入理解. 这一趋势为语义建模的推广提供了现实基础: 语义信息的构建成本较低, 具备良好
的实用性与扩展性. 后续研究也表明, 更系统化地挖掘与利用语义信息具有推动 DMCK 向下一阶段演进的潜力.

4.1 系统语义感知模型检验框架
我们深入分析了系统语义感知 DMCK 的相关工作, 并从 DMCK 的演化视角出发, 将其框架划分为 3 层 (如
图 5 所示). 其中, 系统语义感知 DMCK 位于中间层, 研究重点在于系统性引入语义信息以增强状态约减能力.

形式化 选主 日志复制 集群管理 快照同步 …
建模 协议 协议 协议 协议

语义感知 事件独立性 状态对称性 协议特定 垂直领域
策略 语义 语义 语义 语义

通用探索 状态搜索 动态偏序 对称性 局部状态 …
技术 算法 约减 约减 划分
图 5 系统语义感知的模型检验框架