Page 296 - 《软件学报》2026年第5期
P. 296

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


                 的后续研究 LMC    [57] 主要聚焦于优化状态探索, 将网络状态与节点状态分离, 使网络历史消息在全局共享且不被删
                 除, 仅依赖节点状态进行状态等价判定. 这种方式减少了一定深度内的状态数量                        (但在更深层次可能导致状态空间
                 急剧膨胀), 加快了在线模型检验在限定时间内的深度探索.
                    McErlang [47] 是一个针对 Erlang 程序的模型检验工具, 专门用于分布式系统协议的验证. 它提供了一套运行时
                 API, 替换了标准 Erlang 运行时系统中与分布式、并发和通信相关的部分. McErlang 自动将用户提供的                      Erlang 协
                 议代码翻译为使用该运行时 API 的形式, 并结合用户提供的环境代码进行模型检验, 后者可用于定义节点故障、
                 网络错误等事件. 在此过程中, McErlang 通过模拟进程执行来实现程序的确定性模拟执行.
                    DSLabs [69] 主要用于分布式系统教学, 提供测试、调试和模型检验框架, 与 Mace 类似. DSLabs 通过 Java 接口
                 定义节点变量状态及原子事件           (主要为消息处理和超时处理), 使用者专注于协议实现                (如 Paxos、主备系统), 而框
                 架负责操控网络、时钟、随机数和错误等不确定性因素并触发相关事件代码执行. DSLabs 采用基于状态的模型
                 检验方法, 将协议级状态存储并加入探索队列, 并提供可视化调试器, 便于教学和分析.
                    从以上基于状态的确定性模拟执行技术的工作可以看出, 这些工作原理上与传统模型检验技术相似, 其优势
                 在于能够直接运行真实代码, 从而发现代码中的实际缺陷. 然而, 其劣势也同样明显: 一方面, 这些技术通常需要对
                 现有系统进行大量手工修改以进行移植, 或者限制使用特定语言或框架编写新系统; 另一方面, 基于状态的确定性
                 模拟执行技术通常将分布式系统模拟为单进程运行                  [42−44,52,59,69] , 与真实分布式环境存在差异, 而对多个节点的状态
                 进行一致性快照既低效又难以精确实现              [50,57] . 这些问题限制了该类技术在学术界的进一步发展和应用, 且尚未在
                 工业界得到广泛应用.
                  3.1.3    基于事件的确定性模拟执行技术
                    基于事件的确定性模拟执行技术由             VeriSoft 首创, 该方法识别到基于状态的确定性模拟执行在管理复杂内存
                 状态时存在挑战      [77] , 尤其是对使用任意编程语言编写的程序, 例如 CMC 涉及复杂的状态标准化. 尽管 JPF 和                 Mace
                 通过运行时直接管理状态, 在一定程度上规避了状态管理问题, 但其适用范围仅限于特定语言和框架.
                    与基于状态的确定性模拟执行技术的状态回溯方法不同, 基于事件的技术通过在相同初始状态下确定性重放
                 相同的事件序列来恢复系统状态, 从而避免了直接管理分布式系统全局一致内存状态的复杂性和开销. 基于事件
                 的确定性模拟执行技术的优势影响了后续工作的技术选型, 例如 Chess                   [48] 以及 MaceMC, 即使其所依赖的 Mace 框
                 架支持基于状态的确定性模拟执行. 许多后续              DMCK  工具采用了基于事件的确定性模拟执行              [11,40,49,56,64,67,71,73] .
                    在技术实现上, 基于事件的确定性模拟执行主要依赖截获/插桩技术, 使得被测系统中与特定事件相关的代码
                 确定性模拟执行. 根据截获位置在操作系统底层还是应用程序上层, 可将其分为两类: 通用型技术和精准型技术.
                    ● 通用型技术    [48,49,71] : 截获被测系统与操作系统或运行时环境交互的接口, 使得被测系统代码无需修改或仅需
                 少量修改, 对被测系统具有较好的透明性. 然而, 由于事件的执行受环境间接控制, 可能存在操控精度问题, 并且新
                 增事件支持可能需要修改         DMCK.
                    通用型技术的核心特点是无需修改被测系统代码即可实现确定性模拟执行, 从而更易适配新系统, 并使被测
                 系统的运行环境更接近真实情况. 程序的执行受操作系统或运行时环境的影响, 例如超时、消息接收、磁盘读写、
                 线程调度等, 在底层均由操作系统控制. 因此, 通用型技术通过直接截获操作系统或运行时接口来操控节点内的不
                 确定性, 而无需修改被测系统代码. 同时, 在分布式环境中, 与错误相关的不确定性事件                         (如节点故障和网络异常)
                 可通过错误注入进行模拟. 典型采用该技术的工作包括 MoDist                [49] 和 SandTable [71] .
                          [49]
                    MoDist  是首个通用型 DMCK, 仅需提供配置文件即可验证未经修改的分布式系统. 它在 Windows 操作系
                 统与被测应用程序之间插入了一个轻量级截获层, 以截获应用对 WinAPI 的调用, 并具备较全面的截获能力, 支持
                 对网络、时间、文件、内存、线程及错误注入等全局和局部事件的操控. 针对 Windows 复杂的异步网络                               API 带
                 来的挑战, MoDist 采用代理线程机制, 将网络操作从目标线程中分离, 使所有网络交互均由模型检验后端控制.
                 MoDist 模拟了分布式系统可能遇到的多种错误事件, 包括节点故障、网络异常及 WinAPI 调用失败等. 此外,
                 MoDist 还针对确定性模拟执行的效率进行了优化, 例如通过推进虚拟时钟触发超时事件以加快时间推进, 并利用
                 静态分析确定超时事件的触发值. 尽管如此, MoDist 仍然存在一些局限性, 例如它依赖于 Windows API 截获和控
   291   292   293   294   295   296   297   298   299   300   301