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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2026,37(5):2167−2201 [doi: 10.13328/j.cnki.jos.007580] [CSTR: 32375.14.jos.007580] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
分布式系统模型检验技术研究进展

唐瑞泽, 黄 宇, 欧阳凌志, 程 潜, 张宇奇, 马晓星

(计算机软件新技术全国重点实验室 (南京大学), 江苏 南京 210023)
通信作者: 黄宇, E-mail: yuhuang@nju.edu.cn

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

中文引用格式: 唐瑞泽, 黄宇, 欧阳凌志, 程潜, 张宇奇, 马晓星. 分布式系统模型检验技术研究进展. 软件学报, 2026, 37(5): 2167–2201.
http://www.jos.org.cn/1000-9825/7580.htm
英文引用格式: Tang RZ, Huang Y, Ouyang LZ, Cheng Q, Zhang YQ, Ma XX. Research Progress on Distributed System Model
Checking Technologies. Ruan Jian Xue Bao/Journal of Software, 2026, 37(5): 2167–2201 (in Chinese). http://www.jos.org.cn/1000-
9825/7580.htm

Research Progress on Distributed System Model Checking Technologies
TANG Rui-Ze, HUANG Yu, OUYANG Ling-Zhi, CHENG Qian, ZHANG Yu-Qi, MA Xiao-Xing
(State Key Laboratory for Novel Software Technology (Nanjing University), Nanjing 210023, China)
Abstract: Distributed systems serve as the core of modern computing infrastructure, making their correctness essential. However, the high
nondeterminism in the computing environment of distributed systems, combined with the complexity of code design and implementation,
makes the correctness verification of distributed systems a significant challenge. Distributed system model checking (DMCK) enables the
discovery of deep bugs, deterministic reproduction of bugs in real systems, and repair correctness verification by exhaustive code-level
state exploration, thereby addressing the typical problems of distributed systems, such as difficult discovery, diagnosis, and repair. This
study provides a systematic summary of the research progress in DMCK. Centering around the trade-off between “state explosion” and
“manual effort”, it categorizes the development of DMCK into three stages. The first stage focuses on deterministic simulation execution
and state space exploration technologies that make DMCK effective. The second stage introduces a small amount of artificial modeling to
leverage system semantics for alleviating state explosion, and the third stage aims to enhance the interaction between the model layer and
code layer to improve code-level model checking efficiency. Finally, based on the summary of existing work, this study discusses the
current limitations of DMCK and promising development directions in the future.
Key words: distributed system; model checking; correctness; bug detection; state space explosion; formal specification

* 基金项目: 国家杰出青年科学基金 (62025202); 国家自然科学基金 (62372222); CCF-华为胡杨林基金形式化专项 (CCF-Huawei
FM202505)
收稿时间: 2025-04-18; 修改时间: 2025-06-16; 采用时间: 2025-12-02; jos 在线出版时间: 2026-01-28
CNKI 网络首发时间: 2026-01-29