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

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

表 1 信号时序逻辑公式的布尔语义和定量语义

布尔语义 定量语义 (鲁棒性)
w,t ⊨ true ρ(true,w,t) = ⊤
w,t ⊨ θ(X) ⩾ d ⇔ θ(w(t)) ⩾ d ρ(θ(X) ⩾ d,w,t) = θ(w(t))−d
w,t ⊨ ¬φ 1 ⇔ w,t ⊭ φ 1 ρ(¬φ 1 ,w,t) = −ρ(φ 1 ,w,t)
w,t ⊨ φ 1 ∨φ 2 ⇔ w,t ⊨ φ 1 ∨w,t ⊨ φ 2 ρ(φ 1 ∨φ 2 ,w,t) = max{ρ(φ 1 ,w,t),ρ(φ 2 ,w,t)}
′ ′
w,t ⊨ φ 1 U I φ 2 ⇔ ∃t ∈ {t +i|i ∈ I},w,t ⊨ φ 2 ′ ′′
ρ(φ 1 U I φ 2 ,w,t) = sup min{ ρ(φ 2 ,w,t ), inf ρ(φ 1 ,w,t )}
t ′′ ∈[t,t ′ )
′′ ′ ′′ t ′ ∈{t+i|i∈I}
∧ ∀t ∈ [t,t ),w,t ⊨ φ 1

在此基础上, 我们给出 CPS 系统的反例生成 (falsification) 问题的定义.
问题定义: CPS 系统反例生成. 给定 CPS 系统的模型 M 与规约 φ, 反例生成旨在模型 M 中找到违背规约 φ 的
不安全行为. 譬如给定 CPS 系统的混成自动机模型 H = (X,Q,F,Inv,E,G,R,Q ,Q ) 和信号时序逻辑规约 φ, 反例生
f
0
H 中找到合法的系统行为, 使得此时系统的行为轨迹 (即系统状态的信号) w ⊭ φ.
S
成的目标为在混成自动机
针对上述 CPS 系统的反例生成问题, 基于路径的反例生成方法的基本框架如图 1 所示. 这类方法在底层根据
0 Q 中的节点的系统路径, 在顶层针对每条系统路径依次进行
f
系统的混成自动机模型生成从 Q 中的节点出发到达
基于优化的路径反例生成, 搜索寻找该路径上合法但违背目标规约的不安全行为.

② 基于优化的路径反例生成
最优解满足 反例生成成功
 r<0 找到不安全行为
STL 目标规约 φ ≤0 <
最优解不满足,
SAT 编码排除路径 p i
存在路径 p i
不存在路径 反例生成结束
① 基于 SAT 的路径生成 未找到不安全行为
混成自动机
图 1 基于路径的 CPS 系统反例生成方法框架

具体来说, 底层的路径生成可以通过对自动机的离散图结构进行可满足性问题 (SAT) 编码和求解得到, 详细
的形式化定义可见文献 [27]. 通常情况下, 基于路径的方法仅考虑有限步数内的路径以控制复杂度, 即限制路径中
离散跳转次数上限, 这与实际应用中系统通常在有限的时间和资源内运行也是相符合的.
顶层的路径反例生成则是基于路径约束的不满足度 [13] 以及信号时序逻辑的定量语义, 将路径上合法但违背
STL 规约的行为搜索问题转化成了多目标优化问题进行求解的. 其中, 路径约束不满足度 ,w S ). 用于衡
(x 0 ,p i ,τ)
D(C p i
量系统行为 w S 是否是路径 p i 上的合法行为, 即衡量该行为不满足定义 3 中的路径 p i 上的所有不变式及转移
(x 0 ,p i ,τ)
卫式约束 的程度. 路径约束不满足度越大则路径约束的违背程度越严重, 当且仅当不满足度 ,w S ) ⩽ 0
(x 0 ,p i ,τ)
D(C p i
C p i
时, 系统行为 w S 是合法行为. 关于不满足度更详细的形式化定义可见文献 [13]. 而 STL 规约 φ 的违背程度则
(x 0 ,p i ,τ)
可基于信号时序逻辑的定量语义, 由规约 φ 在系统行为 w S 下的鲁棒性 ρ(φ,w S ) 来衡量. 因此, 针对底层生成
(x 0 ,p i ,τ) (x 0 ,p i ,τ)
的每条路径 p i , 顶层采用优化算法最小化路径约束 C p i 的不满足度 D(C p i ,w S ) 以及系统规约 φ 的鲁棒性 ρ(φ,w S ).
(x 0 ,p i ,τ) (x 0 ,p i ,τ)
如图 1 所示, 若顶层的路径反例生成模块在给定的优化算法迭代次数内, 找到一组由系统变量初值以及路径
节点停留时间构成的最优解 (x 0 ,τ), 使得 ,w S ) ⩽ 0 且 ρ(φ,w S ) < 0, 则反例生成成功, 找到了违背目标规
(x 0 ,p i ,τ) (x 0 ,p i ,τ)
D(C p i
约的系统合法行为; 否则, 将该路径的 SAT 编码后取反, 加入底层路径生成模块的 SAT 问题编码中, 然后在底层
继续通过 SAT 求解来生成还未检查的路径. 若底层 SAT 求解找到路径, 则顶层继续进行基于优化的反例生成, 否
则, 说明所有系统路径都已被检查, 反例生成结束, 未找到不安全的系统行为.

2.2 多臂老虎机问题
多臂老虎机 (multi-armed bandit) 问题是概率论中的一个经典问题 [34] , 其目标是在多个选择 (即多个老虎机的