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