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

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

生成优化算法的迭代次数上限相同, 这导致具有潜力的路径对应的状态空间可能不能被充分探索. 针对这一问题,
我们提出了多臂老虎机问题算法指导的路径动态选择的反例生成方法, 通过在每一轮选择上置信界更大、更有潜
力的路径来进行基于优化的反例生成, 从而尽可能地平衡对系统状态空间的探索和利用, 自适应地动态调整对不
同路径上的行为进行探索的资源分配, 最大化状态空间的探索效率. 第 3.2 节将具体介绍我们的路径动态选择反
例生成算法.

3.1 面向目标规约的路径快速探索与过滤
在基于路径的反例生成方法里, 针对底层生成的路径进行基于优化的反例生成过程通常是该方法的主要时间
开销来源. 如果能在反例生成前就排除部分路径, 可以有效缓解路径爆炸问题, 提高反例生成的效率. 本节将介绍
基于如何根据反例生成的目标规约 φ, 高效地过滤一定不存在违背目标规约的合法行为的系统路径.
根据反例生成的问题定义, 需要寻找系统合法但不安全的行为 w S (x 0 ,p,τ) ⊭ φ, 即 w S (x 0 ,p,τ) ⊨ ¬φ. 而根据定义 3, 给定
N S S p 上各节点时的不变式和
系统路径 p = {q j } , 其上行为 w 是系统合法行为要求 w ⊨ C p , 其中, C p 为在路径
0 (x 0 ,p,τ) (x 0 ,p,τ)
转移卫式约束. 因此, 当 C p 中的约束与时序规约 ¬φ 冲突时, 路径 p 上一定不存在违背目标规约的合法系统行为,
即该路径可以被直接过滤, 无需进行反例生成.

基于信号时序逻辑的语义, 我们设计了根据检测路径约束 C p 与时序规约 ¬φ 是否一定冲突来过滤路径的算
法, 伪代码见算法 1. 该算法采用动态规划的思想, 为路径上的每个节点以及规约 ¬φ 的语法解析树中的所有子式
分别判断, 子式在节点是否一定成立或冲突. 每个子问题的判断都基于 SMT 求解器的结果或其他子问题的判断结
果. 其中, SMT 求解器是一种用于确定逻辑公式在给定理论下是否可满足的工具, 其返回结果通常有以下几种情
况: SAT 表示给定的逻辑公式是可满足的, 即存在一种变量赋值使得所有的约束条件都能被满足; UNSAT 表示给
定的逻辑公式是不可满足的, 即一定不存在任何一种变量赋值能使所有的约束条件都被同时满足; UNKNOWN 表
示求解器无法确定给定的逻辑公式是否可满足.
算法 1. 面向目标规约的路径过滤.
N
输入: 待检查路径 p = {q i } , 反例生成的目标规约 φ;
0
p true 表示过滤,
输出: 是否过滤路径 , false 表示保留.
1. Function pathFilter( φ, p)
2. φ neg = transform( ¬φ); ▷ 通过等价转换将否定符号 ¬ 移至谓词前
3. ϕ = parse( φ neg ); ▷ 存储 φ neg 的语法树中的所有公式 (沿语法树自顶向下)
[ ]
4. init R |ϕ| [N +1]; ▷ 公式在节点上的冲突表, 1: 总成立, 0: 未知, –1: 冲突
5. for i = |ϕ|−1 to 0 do ▷ 遍历所有公式, 从底层的谓词到顶层的 φ neg 自身
6. for j = N to 0 do ▷ 从路径的最后一个节点到第 1 个节点
]
[
7. if ϕ[i] := true then R i, j = 1; ▷ 总成立
8. else if ϕ[i] := θ(X) ⩾ d then ▷ SMT 检查公式 ϕ[i] 与节点 q j 是否冲突
[ ]
9. if SMTsolver( Inv q j ,Q = q j ,ϕ[i])=UNSAT then R i, j = −1;
[
]
10. else if SMTsolver( Inv q j ,Q = q j ,¬ϕ[i]) =UNSAT then R i, j = 1;
]
[
11. else R i, j = 0; ▷ 未知
[
]
]
[
12. else if ϕ[i] := ¬ϕ[k] then R i, j = −R k, j ; ▷ 根据表 1
]
[
[
]
])
( [
13. else if ϕ[i] := ϕ[k 1 ]∨ϕ[k 2 ] then R i, j = max R k 1 , j ,R k 2 , j ;
14. else if ϕ[i] := ϕ[k 1 ] U I ϕ[k 2 ] then ▷ 根据表 1
]
[
(
])
[
15. R i, j = min 0,R k 2 , j ;
[ ] ( [ ] [ ])
16. if j < N then R i, j = max R i, j ,R i, j+1 ;