Page 172 - 《软件学报》2025年第8期

王佳宛 等: 基于混成自动机路径过滤与动态选择的 CPS 系统反例生成 3595

此, 图上的黑色路径上一定不存在违背规约的合法行为, 可以被过滤. 该算法可以保证过滤的路径上一定不存在违
背目标规约的合法行为, 但该算法并不能保证完备. 一方面, SMT 求解器检查谓词公式与约束是否冲突时, 基于的
是其 UNSAT (不可满足) 判断结果, 该结果是可靠但不保证完备的; 另一方面, 由于路径节点和时序算子的时间区
间并无直接对应关系, 所以我们对于包含时序算子的公式的冲突计算也是不完备的. 但值得注意的是, 我们在该算
法第 2 行通过等价转换来移动 ¬φ 的否定符号至谓词前, 形成公式 φ neg , 尽可能地检查出更多的可过滤路径. 此外,
在算法 1 伪代码中, 为与定义 4 中 STL 公式语法相对照, 我们统一给出了包含时序算子的公式的冲突情况计算方
法. 但在实际实现中, 我们可以对包含时序算子 U, G, F, 以及时序算子下标的时间区间 I 是否包含时间 0 等情况进
行分类处理, 从而最大化地过滤路径.

表 2 路径 p 面向规约的过滤计算动态规划表

公式 q 19 q 14 q 9 q 4 q 3 q 2
|x−2| < 0.5 −1 −1 −1 −1 0 0
|y−2| < 0.5 −1 0 0 −1 −1 −1
|x−2| < 0.5 ∧ |y−2| < 0.5 −1 −1 −1 −1 −1 −1
F(|x−2| < 0.5 ∧ |y−2| < 0.5) −1 −1 −1 −1 −1 −1

N C p 的冲突情况计算分
在算法时间开销方面, 该算法采用动态规划思想, 将公式 ¬φ 与路径 p = {q j } 0 上的约束
φ neg 的语法树上形如
解为各个子式在各个节点上的冲突情况计算. 一共有 (N +1)×(m 1 +m 2 ) 个子问题, 其中 m 1 为
θ(X) ⩾ d 的谓词的个数, m 2 为 φ neg 的语法树上其他公式的个数. 对于非谓词公式对应的 (N +1)×m 2 子问题, 算法复
O(1); 对于剩余的谓词公式对应的每个子问题, 算法效率取决于 SMT 求解器的约束求解效率.
杂度均为
由于不同理论的复杂度对 SMT 求解器的性能影响显著: 只包含布尔公式时, 求解效率较高; 包含线性整数算
术时, 复杂度通常为多项式级别; 而涉及非线性算术时, 复杂度显著提升. 因此, 为了能够在不同场景下平衡路径过
滤算法的效率和效果, 在算法 1 的第 9–10 行实现中, 我们提供了路径过滤的配置选项. 用户可根据实际需求自主
选择是否将布尔、线性以及非线性类型的约束交给 SMT 求解器处理. 若选择将所有约束都交给 SMT 求解器求
解, 则可以最大化地过滤路径, 但求解耗时可能较多; 若仅将部分约束交给求解器求解, 则不交给 SMT 处理的约束
冲突情况将被记录为未知, 尽管这可能降低路径过滤算法的完备性, 但可在确保过滤算法正确性 (即过滤的路径上
一定不存在违背目标规约的合法行为) 的同时减少算法耗时. 本文在后续第 4.3 节中将结合实验数据进一步探讨
约束求解与过滤算法的性能权衡. 总体而言, 在实际实验中, 我们发现只考虑布尔或线性约束时, 路径过滤算法通
常都可以在毫秒级完成对路径的快速探索与过滤, 其时间消耗远小于对路径进行基于优化的反例生成, 可以有效
缓解路径爆炸.

3.2 多臂老虎机算法指导的路径动态选择
系统在不同路径上的状态空间通常差异较大, 存在不安全的行为的概率分布也有所不同. 因此, 在探索多条路
径的状态空间以寻找系统不安全行为的过程中, 动态地选择更值得探索的路径进行反例生成, 可以提高发现不安
全行为的效率和成功率.
路径的动态选择可以被视为一个在线优化过程, 每轮优化都需要根据已有信息做出决策, 选择一条路径在该
轮进行探索. 不仅如此, 该优化问题的奖励具有不确定性, 在每次选择路径后采样评估该路径上存在不安全行为的
概率 (奖励) 时, 评估结果是具有不确定性且分布未知的. 因此, 路径的动态选择是一个典型的奖励具有不确定性
的在线优化问题, 传统的梯度下降等优化算法难以适用. 本节将基于定义 5 中介绍的更适用于该类问题的多臂老
虎机经典算法, 提出多臂老虎机算法指导的路径动态选择反例生成方法, 以提高反例生成的性能.
多臂老虎机算法的核心在于解决在空间探索过程中, 对未充分了解的空间的探索与对已获取的探索信息的利
用之间的权衡问题. 类似地, 在基于路径的反例生成问题里, 每一条路径可以视作一个选择, 而对路径上的行为进
行一系列采样模拟并评估行为是否违背规约可以被看作是对该选择的探索. 选择行为空间尚未被充分探索的路径
进行探索, 还是选择已发现很接近不安全行为的路径进行探索, 需要充分权衡. 为使用已有广泛研究和充分理论支