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

唐瑞泽 等: 分布式系统模型检验技术研究进展 2187

组成, AEM 描述触发发散和收敛的条件, 例如 ZooKeeper 依赖 quorum 机制接受写操作并可能导致发散; CEM 则
将 AEM 生成的事件映射到具体操作, 从而探索边缘情况. 通过这一方式, Modulo 避免了冗余探索, 高效发现分布
式系统的收敛性问题.

5 模型层与代码层互动的分布式系统模型检验
系统语义感知的 DMCK 通过人工建模增强了语义信息利用, 但状态爆炸问题依然严峻, 不仅由于状态空间庞
大, 还因探索速度受限. 传统模型检验在状态空间探索方面具备优势, 但人工建模成本高, 且可能与实现代码不一
致. 尽管早期研究尝试从代码中抽取模型 [110–113] , 但尚无工作能直接适用于复杂的分布式系统.
在分布式系统, 尤其是共识协议的实现中, 传统测试难以有效验证设计与实现的正确性. 近年来, 手写核心协
议的模型并进行模型检验逐渐成为业界的最佳实践. 例如, Amazon [22] 、Azure [23] 、MongoDB [24] 和 DeepSeek [26] 等公
司采用 TLA+/PlusCal [34,35,114] 、P [115] 等形式化语言, 验证关键分布式系统的核心模块. TLA+的广泛应用, 既源于其
发明者 Leslie Lamport 在分布式系统领域的深厚影响, 也得益于 TLA+规约语言的轻量设计以及 Amazon 成功经
验的推动 [22] . 鉴于 TLA+对分布式系统验证的深远影响, 本节沿用 TLA+中对规约 (specification) 的广义定义, 即规
约不仅描述系统的正确性属性, 还包括系统行为与环境建模. 此后出现的面向分布式系统的模型检验语言, 如 P 语
言 [115] , 也在一定程度上借鉴 TLA+的设计理念. 然而, 即便形式化模型已广泛存在, 模型与代码之间仍可能存在语
义鸿沟 (semantic gap), 导致行为不一致. 如何实现模型层与代码层有效互动, 既充分发挥模型层模型检验的优势,
又能在实现层实现代码级的模型检验 (DMCK), 成为高性价比的技术方向, 并催生了多项相关研究.
本节将探讨模型层与代码层互动的 DMCK (简称互动式 DMCK) 关键技术, 涵盖规约的内容、定位与语言选
择, 解决模型层与代码层之间语义鸿沟的两种方法, 以及最终在代码层实现互动式执行的机制. 图 7 展示了其整体
框架, 核心思想是通过形式化规约与一致性比对技术, 建立模型与代码之间的有机互动, 并将状态空间探索任务交
由传统模型检验工具完成.

节点1 形式化规约
事件执行/ 状态探索 属性验证
状态恢复 一致性比对 卸载
不确定性截获层 状态约减策略
代码执行 确定性事件模拟 模型状态
操作系统 轨迹 空间 状态遍历算法
DMCK后端引擎
被操控节点 传统模型检验工具
图 7 互动式 DMCK 框架图

5.1 系统建模与规约技术
编写分布式系统规约已成为行业最佳实践, 但如何构建高质量的规约仍面临多个关键问题: 规约应包含哪些
内容? 如何确定规约的层次与粒度? 业界主要采用哪些语言? 本节围绕这些问题, 探讨相关研究的解决方案.
5.1.1 规约的内容
本文沿用 TLA+ 对规约 (specification) 的定义, 将其划分为系统行为、环境和正确性属性这 3 部分, 一个概要
的 Zab 协议的 TLA+ 规约如图 8 所示, 分别体现了消息处理的系统行为、节点宕机的环境行为, 以及仅存在一个
合法主节点的正确性属性.
[8]
系统行为规约描述系统的核心行为, 例如分布式协议 (Paxos 、Raft 、Zab [6,10] 、CRDT [116] 等)、业务逻辑和
[9]
容错机制, 具体内容因系统而异. 环境规约则刻画分布式环境的高度不确定性, 包括网络消息分发、用户负载、节
点故障和网络错误等因素. 正确性属性规约用于定义系统的正确性要求, 通常分为安全性 (safety) 和活性 (liveness),
其详细内容在第 3.3 节已有讨论.