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

3596 软件学报 2025 年第 36 卷第 8 期

撑的多臂老虎机算法来指导我们在路径选择过程中做出最佳权衡, 我们对基于路径的反例生成方法进行分析与
调整.
具体来说, 所有路径都有各自的用于行为空间探索的优化求解器. 为对每次选择探索的路径进行评估, 我们对
该路径执行 k 轮基于优化的反例生成, 即基于其优化求解器采样 k 条该路径上的系统行为进行评估, k 为远小于系统
反例生成全过程的行为模拟次数总上限 K 的固定值. 当某条路径被再次被选择时, 其优化求解器中保留上一轮探
索的最优值等信息. 由于我们的反例生成被转化为了多目标优化问题, 需要同时最小化 ,w S ) 和 ρ(φ,w S ),
D(C p i (x 0 ,p i ,τ) (x 0 ,p i ,τ)
优化目标为 ,w S ) ⩽ 0 且 ρ(φ,w S ) < 0, 因此, 我们将每次路径选择的奖励值设为 , ˜w))−
D(C p i (x 0 ,p i ,τ) (x 0 ,p i ,τ) r( ˜w) = −max(0,D(C p i
+ S 对应的函数值. 奖励值越大, 则路径上的行为越
max(−ϵ,ρ(ϕ, ˜w)),ϵ → 0 , 即 k 轮优化后找到的最优行为 ˜ w = w (˜x 0 ,p i ,˜τ)
接近合法且不安全的系统行为.
由于每轮路径选择后, 基于优化计算路径奖励的代价较大, 涉及对 CPS 系统复杂混成行为的迭代模拟计算,
远大于每一轮的路径选择时对所有路径的奖励分布进行计算排序的耗时, 所以我们采用第 2.2 节介绍的策略计算
复杂度更高但具有更强理论保障的上置信界 (UCB) 算法来指导每轮的路径选择. 我们的路径动态选择的反例生
成过程如图 2 相关部分所示, 对应的算法伪代码见算法 2.

算法 2. 基于多臂老虎机算法指导的路径动态选择的反例生成.
n c, 系统行为模拟的次数
T
输入: 路径集合 P = {p i } , 反例生成的目标规约 φ, 动态选择轮数 , 动态选择的平衡参数
1
上限 K;
输出: 若反例生成成功则返回找到的系统不安全行为, 否则返回空指针.
1. Function pathFalsify( P,φ,T,c,K)
2. for p i ∈ P do ▷ 为每条路径初始化
3. ,φ); ▷ 根据路径约束及目标规约初始化路径的反例生成优化求解器
o i = initOptimizer(C p i
4. N i = 0,R i = 0; ▷ 初始化路径选择次数和奖励估计值
5. for t = 1 to do ▷ 基于 UCB 算法动态选择 T 轮路径进行反例生成
T
6. for p i ∈ P do ▷ 计算每条路径的上置信界
7. if N i = 0 then UCB i = ∞; ▷ 路径还未被选择
√
8. else UCB i = R i +c× 2lnt/N i ; ▷ 根据公式计算上置信界
9. s = argmax UCB i ; ▷ 选择上置信界最大的路径 p s
i
10. ˜ w = −o s .run(K/T); ▷ 继续执行 K/T 轮优化记录路径上最优行为
11. , ˜w))−max(−ϵ,ρ(ϕ, ˜w)); ▷ 计算奖励
r = −max(0,D(C p i
12. if r > 0 then return ˜ w; ▷ 反例生成成功, 找到系统中的不安全行为
13. N s = N s +1;
14. R s = R s +(r −R s )/N s ; ▷ 更新选择的路径的奖励估计值
15. return NULL; ▷ 未找到不安全行为

具体来说, 本文提出的基于路径动态选择的反例生成算法的输入包括路径集合 P, 反例生成的目标规约 φ, 动
K
态选择轮数 T , 平衡参数 c, 以及系统行为模拟的次数总上限 . 首先, 算法为每条路径 p i 初始化优化求解器 , 并
o i
将路径选择次数 N i 和奖励估计值 R i 均初始化为 0 (第 2–4 行). 然后, 基于多臂老虎机问题的 UCB 算法动态选择 T
轮路径并进行基于优化的反例生成 (第 5–14 行). 在每轮动态选择过程中, 算法计算每条路径的奖励上置信界
UCB (第 6–8 行), 并选择 UCB 值最大的路径 p s 进行反例生成. 选定路径 p s 后, 算法运行其反例生成的优化求解器
r (第 10, 11 N s 和
o s , 进行 k = K/T 轮迭代优化以计算选择路径 p s 获得的奖励 行). 随后, 更新选择路径的选择次数
平均奖励 R s (第 13, 14 行). 如果在某轮迭代中, 反例生成的优化求解器找到了系统的不安全行为, 即奖励 r > 0, 则
反例生成成功 (第 12 行); 否则, 在所有路径轮次结束后返回反例生成失败, 未找到系统中的不安全行为