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

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

表 1 确定性模拟执行技术典型工具的支持能力、实现技术及应用范围 (续)

发表会议及 技术实现 技术 全局事件支持 局部事件支持
工具 事件操控方式 被测系统
年份 分类 特性 能力 能力
部分支持 (消 部分支持 (仅 基 于 Scala语 言 或 Actor-
透明、 在Basset运行时 (基于
[52]
[51]
Basset ASE 2009 基于状态 息事件和客户 支持线程调 Foundry库 实 现 的 演 员
易扩展 JPF) 运行Java程序
端操作) 度) (actor) 编程模型程序
部分支持 (仅
透明、 透明截获了MPI编程 使用MPI接口通信的程序:
[54]
[53]
ISP PPoPP 2009 基于事件 支持消息事 未支持
可适用 接口 ParMETIS、MADRE
件)
部分支持 (仅
易扩展、 为被测系统手动插桩/ C++语言实现的分布式系
[55]
[56]
dBug SSV 2010 基于事件 支持所有类型 资源访问和线
可适用 适配dBug接口 统: PVFS、FAWN-KV
程调度)
取决于 依赖于后端 (MoDist 包 括 MoDist和 Mace论 文
DeMeter SOSP 2011 [40] 基于事件 支持所有类型 支持所有类型
后端 或Mace) 中的被测系统
自动编译到LMC运行
透明、 部分支持 (仅 Mace语言编写的Paxos和
LMC NSDI 2011 [57] 基于状态 支持所有类型 时环境 (基于MaceMC
易扩展 线程调度) 1Paoxs
和CrystalBall)
在 MP-Basset运 行 时
透明、 部分支持 (仅 MP语言编写的程序/协议:
[59]
[58]
MP-Basset DSN 2011 基于状态 支持所有类型 (基于Basset) 运行MP
易扩展 线程调度) Paxos、Multicast等
语言编写的程序
透明、 部分支持 (仅 基 于 MP-Basset运 行 MP语言编写的程序/协议:
[58]
[60]
DBSS SRDS 2013 基于状态 支持所有类型
易扩展 线程调度) 时 Paxos、Zab等
部分支持 (消
[61]
ASE 2013 , 部分支持 (仅 运 行 于 net-iocache扩 Java语言编写的client/server
net-iocache [62] 基于状态 透明 息事件和客户
TSE 2014 , 线程调度) 展JPF运行时 架构的程序: HTTP server等
端操作)
部分支持 (仅
透明、 部分支持 (仅 自动对Erlang代码插 主要面向Erlang编写的演
[63]
[64]
Concuerror ICST 2013 基于事件 支持消息事
可适用 线程调度) 桩 员 (actor) 模型程序
件)
易扩展、 基于AspectJ手动插桩 ZooKeeper、Hadoop、
SAMC [65] OSDI 2014 [11] 基于事件 支持所有类型 未支持
可适用 Java代码, 错误注入 Cassandra
ZooKeeper、Hadoop、
FlyMC [66] EuroSys 基于事件 易扩展、 支持所有类型 未支持 手动插桩 (Java, C++), Cassandra、Spark、
2019 [67] 可适用 错误注入
LogCabin、Kudu
未支持 (被测 学生基于DSLabs接口实现
DSLabs [68] EuroSys 基于状态 透明、 支持所有类型 系统是单线程 自动编译到DSLabs运 的分布式系统/协议: 键值
2019 [69] 易扩展 行时
的) 存储、Paxos等
透明截获应用程序与 实现了关键分布式协议的
[70] EuroSys 透明、
SandTable 基于事件 支持所有类型 未支持 操作系统 (POSIX) 的 系 统 : ZooKeeper、 Xraft-
2024 [71] 可适用
交互, 错误注入 KV、RedisRaft等
[72] EuroSys 易扩展、 基于AspectJ手动插桩 实现了关键分布式协议的
Remix 基于事件 支持所有类型 支持所有类型
2025 [73] 可适用 Java代码, 错误注入 系统: ZooKeeper
3.1.2 基于状态的确定性模拟执行技术
基于状态的确定性模拟执行技术遵循传统模型检验的思路, 将分布式系统建模为状态机, 其中状态和事件是
核心概念. 每个事件触发状态转移, 系统完整地记录当前状态, 并据此判断可调度的下一个事件. 调度器通过状态
比对识别已探索的状态, 避免重复执行. 在状态回溯时, 直接恢复先前存储的状态. CMC [42,43] 、Mace [44,45] 、基于
Java PathFinder (JPF) [74] 的 Basset [52] 等一系列典型研究均采用此方法, 并提供运行时环境来执行事件及管理状态的
保存与恢复. 由于分布式系统普遍采用事件驱动机制, 这些工作通常通过一套接口执行事件触发的代码, 但适配代
码到接口的方式有所不同, 主要分为两类.
● 手动移植现有系统的事件处理函数至运行时 [42,43] : 这种方式透明性较差, 适配新系统需要大量修改被测代
码, 但适应性较强.