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

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

● 设计框架接口, 使符合框架规范的程序可直接运行于运行时 [45,47,52] : 这种方式适用性较差, 难以直接应用于
已有系统, 但透明性较强.
状态的保存与恢复主要涉及网络状态与进程状态.
● 网络状态: 包含暂存但尚未送达的网络消息, 这些消息需要缓存, 以便调度器按照不同顺序调度, 从而触发
消息处理事件和模拟网络故障事件 (如消息丢失、乱序、重复、网络分区等).
● 进程状态: 可采用低层次的内存字节流方式编码保存, 或高层次的变量键值对方式编码保存. 对于手动移植
代码的方式, 完整变量值难以直接获取, 通常通过操作系统底层提取堆、栈、静态变量等内存字节流进行存储. 对
于框架化编写的代码, 由于变量受框架管理, 可直接存储变量键值对. 此外, 操控进程状态可用于模拟节点故障、
重启等错误事件.
CMC [42] 观察到分布式/网络系统的核心协议实现 (如 AODV 路由协议) 通常采用事件驱动风格, 因此直接提取
原始系统中的核心协议事件执行代码, 并适配到 CMC 的虚拟运行时环境. 该环境提供最小化的虚拟操作系统接
口, 如时间管理、网络收发等系统调用, 以支持移植代码的执行. CMC 将网络消息状态与所有节点的内存字节流
状态整合为一个整体, 视为整个系统的状态, 并在事件执行时同步恢复网络与节点内存状态. CMC 发现了包括
Linux 在内的重要系统中 AODV 实现的多个缺陷, 并发现了 AODV 协议的深层设计问题, 首次展现了模型检验在
复杂分布式协议代码级验证上的有效性. CMC 后续工作 [43] 进一步用于 Linux TCP 网络协议的验证, 过程中发现手
动提取和适配复杂代码容易引入难以调试的假阳性缺陷. 最终, 研究者选择直接在 CMC 虚拟执行环境中运行修
改版的用户态 Linux 内核, 并成功发现了 4 个缺陷. CMC 在真实复杂分布式代码验证中展现了有效性, 但该方法
存在两个主要挑战: 1) 手动适配过程工作量大且易出错; 2) 状态保存和恢复的精确控制困难, 细微的内存比特变
化 (如堆区动态分配顺序) 可能导致逻辑等价状态被误判为不同状态. 为减少代码剥离原始环境带来的问题, CMC
后续采用直接运行 Linux 的方式, 但适配 Linux 仍需大量工作量. 此外, CMC 通过状态标准化 (state canonicaliza-
tion) 合并等价状态, 但该过程仍依赖大量人工干预.
JPF [74] 是 NASA 开发的 Java 语言模型检验工具, 提供一个可控制不确定性和支持状态回溯的 Java 虚拟机.
JPF 主要操控线程调度等局部事件, 不支持 DMCK 所需的全局事件 (如网络收发和错误事件). 它维护了线程调用
栈、静态与动态对象的状态信息, 从而支持状态比对和去重. JPF 的虚拟机工作方式类似于 CMC 提供的虚拟运行
时环境, 由于 Java 程序本身运行于虚拟机, JPF 避免了 CMC 在适配新系统时面临的大量人工适配和状态标准化
问题. 扩展 JPF 以支持 (部分或全部) 全局事件的工具包括如下 3 种.
● Basset [52] : 提供了一个框架, 支持基于 Scala 或 ActorFoundry Java 库的 Actor 计算模型, 使得 Actor 之间的消
息交互可被确定性操控. Basset 主要增加了对网络消息调度的控制, 但仍不支持错误事件的操控.
● MP-Basset [59] : 在 Basset 基础上扩展, 增强了对基于消息传递 (message passing) 的容错分布式协议 (如
Paxos) 的检验能力, 支持节点失效和网络错误模拟. 该研究更侧重高效状态探索方法, 错误模拟简化为不调度特定
节点. 其后续研究 LPOR [75] 和 DBSS [60] 进一步优化了状态探索策略.
● net-iocache [61] : 提供了一个 JPF 插件, 使得 JPF 能够处理单线程管理多个非阻塞网络连接的情况. 该工具通
过缓存网络通信历史, 使 JPF 在状态回溯时能够重用历史数据. 后续研究 [62] 进一步扩展了其适用范围. 然而, net-
iocache 及后续工作不支持分布式系统中的典型错误场景.
Mace 语言框架 [44] 源自 Macedon 原型 [76] , 扩展了 C++ 以提供分布式系统编程的语言级支持. Mace 采用状态-
事件-转移 (state-event-transition) 模型, 将分布式系统建模为状态机, 并提供统一框架支持代码事件、网络事件和
错误事件的操控. 开发者通过 Mace 框架定义状态变量和状态转移, 每个事件被原子执行 (相当于控制了节点内线
程调度), 内置模型检验工具在事件执行后记录节点变量和网络消息队列的完整状态, 以支持状态探索. CrystalBall [50]
基于 Mace, 主要用于深度在线调试 (deep online debugging) 和执行操控 (execution steering), 可预测并规避可能导
致不一致的执行路径. 由于 CrystalBall 针对已部署的运行中分布式系统, 其面临无法高效获取全局一致快照的问
题. 为此, CrystalBall 采用局部快照方案, 每个节点仅采集与其直接通信的邻居节点状态, 并通过独立线程执行模
型检验, 向运行时反馈需要规避的路径. 采集快照时, CrystalBall 使用 fork 技术复制节点的虚拟内存. CrystalBall