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

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

的执行顺序, 通过确定性模拟执行技术来执行调度的事件. 为应对状态爆炸问题, 研究者们提出了多种优化技术,
包括状态空间约减技术和探索效率优化. 接下来, 我们将分别讨论这些技术的实现和优化.
3.2.1 状态空间搜索方法
状态空间搜索方法可分为有状态搜索 (stateful search) [91] 和无状态搜索 (stateless search) [77] . 根据定义, 有状态
搜索的下一次搜索依赖于历史状态, 即之前探索的路径; 而无状态搜索不记录历史状态, 每次搜索的决策独立于之
前的探索过程.
第 3.1 节中提到确定性模拟执行技术分为基于状态和基于事件两种方法. 在状态空间搜索上, 基于事件的方
法由于缺乏状态保存能力, 只能采用无状态搜索; 而基于状态的方法具备完整的状态保存能力, 通常采用有状态搜
索, 也可采用无状态搜索.
有状态搜索 (stateful search): 有状态搜索的原理与传统模型检验搜索算法类似, 算法从一个初始状态开始, 搜
索并探索整个状态空间, 算法伪代码如图 3 所示 [77] . 算法维护两个集合: 已探索状态集 (Explored) 和未探索状态
集 (Unexplored). 初始状态 s 0 加入未探索集合中 (第 2 行). 然后, 算法循环从未探索状态集取出一个状态. 如果该
状态不在已探索集合中, 则对其进行探索并将其加入已探索集合 (第 3–13 行). 对被探索的状态的所有可执行/使
能 (enabled) 转移进行执行并产生新的后继状态, 并将这些后继状态加入未探索集合中 (第 7–11 行). 循环此过程
直到未探索状态集为空.

1 Initialize: Unexplored is empty; Explored is empty;
2 add s 0 to Unexplored;
3 Loop: while Unexplored ≠ do {
4 take s out of Unexplored;
5 if s is NOT already in Explored then {
6 enter s in Explored;
7 T = enabled(s);
8 for all t in T do {
9 s′ = succ(s) after t;
10 add s′ to Unexplored;
11 }
12 }
13 }
图 3 有状态搜索算法 (引自 VeriSoft [77] )

下面解释 DMCK 中有状态搜索的具体实现细节, 不同实现方式可能影响探索效率和缺陷发现速度.
● 状态取出顺序影响缺陷发现的路径和速度 (第 4 行). 深度优先搜索 (未探索状态集为 LIFO 栈) 优先探索较
深状态, 可更快触及长路径缺陷. 广度优先搜索 (FIFO 队列) 发现的缺陷触发路径最短, 便于分析, 但当缺陷位于较
深层时, 探索时间可能更长. 随机策略可提高状态多样性, 加快代码覆盖率. 启发式策略需结合领域知识, 优先探索
高价值状态, 可提升特定缺陷发现速度, 并可与其他搜索方式结合 [42] .
● 状态比对用于状态去重 (第 5 行). 最基本的方法是计算状态哈希进行比对, 更高级的方法是在计算哈希前
进行状态标准化, 例如利用节点角色对称性将等价状态归一化 [74] , 以进一步减少冗余状态.
● 状态表示方式影响状态空间规模. 最直接的方法是记录系统内存信息 [42] , 更精简的方法是仅存储协议关键
变量状态 [44,69] , 可减少状态数量和内存占用, 但可能误判不同状态为相同, 导致遗漏.
● 可执行/使能转移 (enabled transitions) 由确定性模拟执行器报告 (第 7 行). 例如, 可触发的超时、可送达的
消息和可注入的错误等. 由于不确定性, 多个动作可能同时使能, 确定性模拟执行器通常使用 Toss/Choose [42,45,77] 函
数, 在指定范围内依次返回不同值 (类似 fork 效果), 确保探索所有路径.
无状态搜索 (stateless search): 无状态搜索按定义不记录历史状态, 每次探索的决策独立于此前的执行路径. 这
种策略虽实现简单, 但会导致等价状态无法区分而被多次重复遍历, 使状态/路径空间急剧增长. 此外, 无状态搜索
回溯时需从初始状态重新执行事件序列来生成状态, 增加了 CPU 开销. 因此, 纯粹的无状态搜索算法在实践中效