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

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

2 分布式系统模型检验技术综述框架

传统模型检验技术通过穷尽式搜索系统的状态空间, 具备两大核心优势: 1) 严格的正确性保障: 能够对系统
的所有可能状态进行穷举验证; 2) 高度自动化: 用户只需提供系统的模型和正确性规约, 即可通过“push-button”式
的方式自动完成验证. 然而, 该方法存在显著不足. 首先, 模型与实际系统之间存在语义鸿沟, 模型的正确性并不意
味着系统实现正确. 其次, 状态爆炸问题严重, 使得其正确性保障通常需在一定限制条件下才能成立. 这些问题成
为模型检验技术在软件系统中实际应用的主要障碍.
分布式系统模型检验技术 DMCK 是针对分布式系统的代码级模型检验, 对代码所有可能执行路径对应的状
态空间进行系统性、穷尽式探索. DMCK 从根本上解决了抽象模型与具体实现之间的语义鸿沟问题, 避免了模型
检验中的转译错误 (transcription error), 并保留了传统模型检验技术的高度自动化优势. 然而, 由于代码实现包含
复杂具体细节 (例如多线程调度、磁盘异步读写、超时等机制) 以及分布式系统环境高度不确定性 (例如消息延
迟与乱序、节点宕机、用户请求), DMCK 面临比传统模型检验更严重的状态空间爆炸问题. DMCK 的状态空间
爆炸不仅体现在状态数量的指数级增长, 还体现在探索速度的显著降低. 由于 DMCK 需要实际执行代码, 其状态
空间探索的开销远高于传统模型检验在抽象模型上的状态搜索. 各种 DMCK 状态空间探索优化技术被提出来缓
解状态爆炸问题.
早期研究为了让 DMCK 具备可行性, 研究的技术主要包括控制分布式系统中的不确定性的确定性模拟执行
技术 (deterministic simulation)、系统性探索状态空间的搜索算法和通用的状态空间约减算法. 通过这些技术,
DMCK 工具去除了传统模型检验中的建模成本, 验证结果直接反映到代码中. 这些技术不仅奠定了 DMCK 的基
本能力, 也为后续研究奠定了基础.
由于 DMCK 技术面临的状态爆炸问题更为严重, 所以通用的优化技术迅速遇到瓶颈. 此时的突破口在于利用特
定系统的特定语义知识, 例如系统事件的独立性和对称性, 针对性地、垂直性地进行约减状态空间. 语义感知的优化
对于效率的提升, 是以验证技术的通用性与自动化程度为代价的. 但是针对分布式系统正确性保障的迫切需求, 面对
极其严重的状态爆炸问题, 适当牺牲通用性与自动化程度并引入一定人工建模成本是一种有效、高效的权衡.
传统模型检验技术在 DMCK 发展过程中也在进步, 尤其是轻量级建模语言和验证工具链的成熟, 使得复杂的
分布式系统设计及优化得到较低成本验证和较高正确性保障, 这些进步推动了模型检验技术在工业界的广泛应
用 [22−26] . 这一背景下, 模型层与代码层互动的模型检验技术被提出, 该技术通过对二者状态空间的比对, 建立模型
与代码的映射, 使得模型检验结果可反映到代码, 大幅提升了 DMCK 的状态探索效率、有效性和性价比. 从 DMCK
的发展脉络角度来看, 与模型层互动是语义感知优化的更深和更广的应用方式.
本文根据 DMCK 的发展脉络, 将 DMCK 的发展分为 3 个阶段, 如图 1 所示. 这些阶段的发展体现了平衡
DMCK 的自动化程度和状态空间探索效率之间的矛盾的过程, 逐步增加了人工成本但提升了性价比. 下面我们将
遵循这一脉络, 分别介绍具体技术.

第 1 阶段 第 2 阶段 第 3 阶段
无需人工建模
人工建模语义信息
人工建模系统行为
确定性模拟执行技术
状态空间探索技术
系统语义感知优化技术
模型-代码一致性比对技术
自动化程度高 权衡: 人工建模增加
状态爆炸严重 状态爆炸 vs. 人工成本 验证效率提升
图 1 DMCK 技术发展阶段划分示意图

3 传统分布式系统模型检验

尽管传统模型检验技术在分布式协议验证方面取得了显著成功 [36,37] , 但应用于分布式系统实现时, 面临着形