软件学报

作者：唐瑞泽，黄宇，欧阳凌志，程潜，张宇奇，马晓星

单位：唐瑞泽，计算机软件新技术全国重点实验室(南京大学), 江苏 南京 21002311,黄宇，计算机软件新技术全国重点实验室(南京大学), 江苏 南京 21002302,欧阳凌志，计算机软件新技术全国重点实验室(南京大学), 江苏 南京 21002303,程潜，计算机软件新技术全国重点实验室(南京大学), 江苏 南京 21002304,张宇奇，计算机软件新技术全国重点实验室(南京大学), 江苏 南京 21002305,马晓星，计算机软件新技术全国重点实验室(南京大学), 江苏 南京 21002306

关键词：分布式系统;模型检验;正确性;缺陷发现;状态空间爆炸;形式化规约

基金：国家杰出青年科学基金(62025202); 国家自然科学基金(62372222); CCF-华为胡杨林基金形式化专项(CCF-HuaweiFM202505)

分布式系统作为现代计算基础设施的核心, 其正确性至关重要. 然而, 由于分布式系统所处的计算环境中的高度不确定性以及代码设计与实现的复杂性, 验证分布式系统的正确性始终面临巨大挑战. 分布式系统模型检验(DMCK)技术通过代码级的穷尽式状态探索, 能够发现深层缺陷, 在真实系统中确定性重现缺陷并验证修复正确性, 有效应对了分布式系统缺陷“难发现、难诊断、难修复”等典型难题. 系统性梳理了 DMCK 的研究进展, 围绕“状态爆炸”与“人工成本”的权衡, 归纳其发展脉络为3个阶段: 第1阶段聚焦于使 DMCK 有效的代码级确定性模拟执行与状态空间探索技术; 第2阶段通过引入少量人工建模以利用系统语义信息缓解状态爆炸问题; 第3阶段致力于增强模型层与代码层的交互能力以进一步提升代码级模型检验效率. 最后, 在总结既有工作的基础上, 探讨了目前DMCK 的局限和未来可能的发展方向.

来源：2026年第5期

《软件学报》期刊编辑部

查看软件学报杂志2026年第5期