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

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

式化建模成本和模型与真实系统偏差等问题. 这促使研究者探索直接以代码作为模型的验证方法, 从而避免建模
成本和模型偏差. 本节主要介绍 DMCK 发展的第 1 阶段, 该阶段的研究重点在于使 DMCK 具备可行性, 即无需人
工建模即可进行模型检验, 且具有有效性和通用性, 我们将其归类为传统分布式系统模型检验技术.
传统模型检验技术通常基于抽象形式模型, 通过特定的检验器进行分析, 从形式化语言设计到支撑工具链实
现, 全流程支持对状态空间的可控且高效的穷尽式探索. 然而, 当模型检验技术应用到真实代码时, 面临两大关键
挑战: 1) 分布式系统中存在来自节点间通信与节点内部执行环境的高度不确定性, 而主流编程语言与运行时环境
并未为其提供可控穷尽式探索的支持. 为了系统性地枚举所有可能的执行路径, DMCK 需解决如何对系统所面临
的各种不确定性进行确定性模拟的问题; 2) 分布式系统中复杂的代码实现与环境不确定性共同加剧了状态空间爆
炸问题, DMCK 需解决如何高效探索状态空间并执行属性验证的问题. 后续各节将围绕上述挑战, 分别介绍确定
性模拟执行、状态空间探索与属性验证等关键技术. 图 2 展示了传统 DMCK 框架的整体架构, 分为被控节点与
DMCK 后端引擎两部分, 图中展示了各关键组件及其交互关系. 其中, 被控节点内的图标分别表示线程、时钟和
网络消息包, 由不确定性截获层进行控制.

节点1 属性验证
事件执行/ 确定性事件模拟
状态恢复
不确定性截获层 状态约减策略
使能事件/
操作系统 节点状态 状态遍历算法
被操控节点 DMCK后端引擎
图 2 传统 DMCK 整体架构图

3.1 确定性模拟执行技术
保障分布式系统正确性的根本挑战在于系统行为的高度不确定性, 主要源于网络通信和外设交互的异步性、
并发性以及运行环境的易错性. 这些因素导致相同输入可能产生大量不同的执行路径, 使得深层缺陷难以触发与
发现. DMCK 技术之所以适用于分布式系统, 正是因为其核心原理“系统性穷尽探索”能够有效应对这种不确定性,
通过对执行过程中的不确定性事件进行控制, 在探索算法的调度下全面覆盖可能的路径.
支撑 DMCK 的首要使能技术是确定性模拟执行 (deterministic simulation). 该技术通过精确控制消息传递、线
程调度与错误注入等关键事件, 将不确定行为转化为可预测、可控的执行过程, 从而支持状态空间的系统性遍历.
具体而言, 确定性模拟执行需支持事件的拦截与调度、状态的保存与恢复, 以便探索过程可在任意状态下回溯与
分叉. 借助这一机制, DMCK 能在可控环境中系统地重现复杂路径, 发现隐藏在边界调度下的深层缺陷.
3.1.1 不确定的环境与确定性的受控执行
为实现这一目标, 首先需要明确分布式系统中的不确定性来源, 并通过特定的劫持技术加以操控. 分布式系
统运行于开放、动态、难控的环境, 不确定性主要来自节点间分布式环境的不确定性和节点内部环境的不确定
性 [38,39] . 前者主要包括消息的异步到达、错误事件、客户端请求等, 后者主要包括线程调度、资源访问、随机数
等. 由于分布式系统往往具有明显的事件驱动特性, 这些环境的不确定性会触发系统中特定事件的执行. 参考
DeMeter [40] , 我们将导致节点间分布式环境不确定性的事件称为全局事件 (global event), 而导致节点内部环境不确
定性的事件称为局部事件 (local event). 由于分布式系统及其核心协议强调节点间分布式环境中的协同交互, 大多
数 DMCK 研究更关注全局事件的受控执行.
全局事件指影响节点间分布式环境的不确定性事件. 在分布式系统中, 这些事件的处理通常涉及系统实现的
核心分布式协议设计, 决定了系统的协同机制和一致性保障. 主要包括以下几类.
● 消息事件: 由于网络延迟, 服务器节点可能在任意时刻接收消息, 而消息的处理可能进一步触发新的消息发
送, 增加系统执行的不确定性.