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

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

程中, DMCK 技术始终围绕“状态爆炸”与“人工成本”之间的权衡展开, 其发展大致可划分为 3 个阶段.
第 1 阶段聚焦于如何“使 DMCK 有效”. 该阶段的核心突破在于确定性模拟执行与无状态搜索技术以及通用
状态约减技术的引入与结合. CMC 通过手动适配支持模拟执行, MaceMC 提供编程框架, MoDist 截获底层系统调
用以提升通用性, dBug 手动精准插桩提升操控精度, 这些工作都控制了分布式系统的不确定性. 同时, VeriSoft 与
DPOR 提出的无状态搜索算法和动态偏序约减技术让 DMCK 技术变得实用并成为基础技术. 在状态约减方面,
DeMeter、CrystalBall 与 LMC 等工作利用节点状态与系统环境的局部性, 缓解了特定场景下的状态爆炸问题.
MoDist 和 FlyMC 等工作优化了代码级状态空间的探索速度. MaceMC 还提出了对活性属性的近似检测策略. 这
一阶段 DMCK 工具开始具备应用于真实系统的能力, 但依赖于不可靠的约减策略来加快缺陷发现速度, 存在遗漏
缺陷的风险.
第 2 阶段致力于“使 DMCK 高效”. 核心思路是将系统语义信息引入状态空间探索过程, 特别是消息传递、崩
溃、同步等事件的对称性与独立性被系统建模并加以利用, 从而实现更大规模的状态约减. 同时, 部分工作利用了
模型检验原理还结合了垂直领域知识, 取得了良好效果. 以 SAMC 和 FlyMC 为代表的工作中, 语义感知能力被集
成进 DMCK 框架, 在不依赖不可靠约减策略的情况下, 成功发现并复现了多个工业级分布式系统的深层缺陷. 尽
管该方法需少量人工标注语义或人工建模, 其性价比已有显著提升.
第 3 阶段聚焦于“增强模型与代码的互动能力”. 该阶段的核心方法是利用形式化规约语言的状态空间探索能
力, 并通过将代码执行与规约状态进行一致性比对, 实现代码与模型的互动验证. 尽管这一路径看似“回退”到早期
需要手动编写规约的模式, 实则得益于形式化方法自身的成熟与普及, 其整体效能和可用性已大幅提升. 代表性工
作包括 SandTable 和 Remix, 以及 DMCK 的派生技术 Smart Casual Verification, 验证了此类方法在实际系统中的
可行性与应用价值.
7.2 局限性和未来展望
DMCK 技术的关键局限在于状态爆炸问题、代码操控成本、建模成本以及模型与代码一致性检查等方面:
1) 缺乏开箱即用的代码级 DMCK 工具: MoDist、DeMeter 未开源、SandTable 依赖规约轨迹、dBug、SAMC、
FlyMC、Remix 等需手动插桩, 使用门槛偏高. CMC、JPF、Mace 等基于状态的系列工具已逐渐淡出学术界与工
业界视野; 2) 状态爆炸问题仍然严重: 虽然已有多种约减与优先探索技术, 但未有工作系统性整合实现, 且实际使
用中依然以“发现缺陷”为主, 难以穷尽整个状态空间; 3) 规约开发存在一定成本: 尽管形式化规约+互动验证的路
径具备较高性价比, 现有方法如 SandTable 和 Remix 等依然需要用户编写规约, 影响其推广与普及; 4) 规约与代码
之间仍存在消除分歧的成本: 尽管互动验证技术已用于缩小差距, 但规约适配、分歧分析仍需人工参与.
上述问题集中反映了当前 DMCK 技术在实用化进程中仍面临多方面挑战, 尤其是在工具可用性、状态空间
探索、规约开发与一致性检查等关键环节尚未形成系统性解决方案. 为进一步推动 DMCK 的发展与落地, 研究者
已开始从多个角度提出改进方向, 未来的演进可围绕以下几个方面展开.
(1) 构建全能、易用的 DMCK 工具: 在确定性模拟执行方面, 目前尚无工具同时具备良好的易扩展性、可适
用性与透明性. 通用型截获技术若能进一步控制底层的不确定性, 有望构建通用的“确定性虚拟机”执行环境.
Antithesis 公司提出商业级实现与此方法类似, 尽管状态空间探索尚非全穷尽, 其确定性控制能力已展示出巨大的
应用潜力. 未来构建类似的开源平台将具有重要研究价值和产业前景.
(2) 集成多种状态约减与优先探索策略: 当前多数模型检验工具仅采用部分特定的状态空间优化技术, 整体上
的状态约减效果与探索效率尚未达到理想水平. 在规约层, TLA+ 等工具已支持多种约减策略, 但如利用事件独立
性的偏序约减 [139] 等仍有待进一步集成 (例如集成到 TLA+ community modules 社区模块 [140] ). 此外, 优先级探索策
略, 如基于 Q-Learning 等机器学习方法的动态调度 [122,141] , 已开始用于提升缺陷发现效率, 展现出良好潜力. 面向
未来, 构建集成多种约减与探索策略的统一工具平台, 将成为该领域的重要研究方向.
(3) 利用大语言模型 (large language model, LLM) 辅助规约开发与语义标注: 规约开发或语义标注是语义感知
和互动式 DMCK 推广中的核心瓶颈. 大语言模型为降低人工成本提供了新路径, 已有初步研究探索从代码自动生