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

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

• 将本文提出的基于路径过滤与动态选择的反例生成技术被扩展实现在工具 SNIFF 上, 并在混成系统的经典
案例上分析验证了该方法的有效性. 实验结果表明该方法可以有效缓解路径爆炸问题, 将 CPS 系统反例生成的成
功率提高到两倍以上并减少时间开销.
本文第 1 节介绍 CPS 系统反例生成的相关工作和研究现状. 第 2 节介绍 CPS 系统的形式化建模与规约描述
语言以及本文涉及的多臂老虎机相关技术的基础知识. 第 3 节介绍本文提出的基于混成自动机路径过滤与动态选
择的 CPS 系统反例生成方法. 第 4 节通过实验具体分析本文技术的有效性. 第 5 节对本文进行总结.

1 CPS 系统反例生成相关工作

CPS 系统反例生成是检测系统行为是否会违背目标规约的有效方法. 现有的反例生成工作大多采用各种优化
算法, 通过最小化目标规约的鲁棒性 [15,16] 来探索系统的状态空间, 寻找系统不安全行为 [6] . Nghiem 等人 [7–9] 提出了
使用各种不同的经典的启发式优化搜索算法, 如蒙特卡洛算法、蚁群算法、交叉熵算法等, 来进行反例生成, 形成
了较为成熟的基于优化算法的 CPS 反例生成工具, 例如 S-TaLiRo [10] 和 Breach [11] . 随后, 一系列工作根据 CPS 系统
反例生成这一具体问题来设计各种不同的状态空间解耦与搜索方法, 以优化反例生成的性能. Mathesen 等人 [17] 基
于信任区间提出了将全局随机优化方法与局部自适应可重启的优化搜索相结合的反例生成方法, Yaghoubi 等人 [18]
提出了将全局的模拟退火优化搜索与基于梯度下降的局部搜索相结合的反例生成方法, Zhang 等人 [19] 则提出了通
过网格分区将全局的蒙特卡洛树搜索和局部搜索相结合的双层反例生成方法. 在此基础上, Wang 等人 [13,14] 将形式
化领域面向路径的方法应用于 CPS 系统反例生成问题, 基于系统模型中的路径对状态空间解耦, 在全局基于路径
遍历探索系统的离散空间, 在局部采用基于分类模型的学习优化方法来搜索各路径上的行为. 该类方法既提高了
反例生成的性能, 又可以有效地支持非确定性系统; 但面向的是具有混成自动机模型的 CPS 系统, 且当模型规模
较大时可能会遇到路径爆炸问题. 相关工具包括 PDF [13] 和 SNIFF [14] .
除了主流的基于优化的反例生成以外, 早期 Plaku 等人 [20] 还提出了基于运动规划的反例生成, 通过提出并使
用模型状态空间覆盖率, 安全规约鲁棒性等指标来指导快速扩展随机树的构造 [21,22] , 从而探索系统模型中的状态
空间, 寻找系统不安全行为. 此外, Zutshi 等人 [23,24] 提出了一类基于梯度的反例生成方法, 基于梯度信息不断优化
调整随机生成的系统行为轨迹片段, 直至最终形成一条完整且不安全的系统行为轨迹. 该方法还与符号执行技术
相结合, 通过分析系统的可达性约束来加快循环迭代找到系统不安全行为的效率 [25] . 由于此类方法需要梯度信息
和可达性分析, 因此通常对系统模型有一定的限制, 难以处理任意非线性系统.
与本文工作最相近的是文献 [13,14] 中提出的基于路径解耦状态空间并基于优化搜索每条路径上的行为的反
例生成工作. 这类基于路径的方法通过状态空间解耦降低了搜索问题的维度和复杂性, 进而提高了反例生成的性
能, 但正如前文所述, 也容易在大规模系统中遇到路径爆炸的问题. 在形式化领域, 路径爆炸是一个常见问题, 指的
是系统中存在大量可能的执行路径使得全面的系统验证或测试变得困难. 为缓解路径爆炸问题, 基于路径剪枝 [26,27] ,
系统模型离散状态合并 [28] , 路径并行探索 [29] 等技术被提出使用. 本文旨在特别针对包含混成行为的 CPS 系统在时
序规约下的反例生成问题, 在基于路径的反例生成工作的基础上, 通过减少需探索的路径数目以及为各路径合理
分配用于探索的资源, 来缓解这类方法中的路径爆炸问题, 进而提升 CPS 系统反例生成的效率和成功率. 实际上,
在 CPS 领域, 基于路径来解耦问题并高效探索状态空间的思路还被应用在相关系统的形式化验证 [30,31] 和控制生
成 [32] 等问题上. 本文提出的路径过滤以及动态选择的优化技术也都可以应用于相关方法, 缓解其中的路径爆炸问题.

2 基础知识

第 2.1 节介绍 CPS 系统反例生成基础知识, 第 2.2 节介绍本文方法涉及的多臂老虎机问题及相关算法.

2.1 CPS 系统反例生成
[3]
混成自动机 (hybrid automata) 是对 CPS 系统中紧密交织的离散和连续行为进行形式化建模的常用语言. 时
序逻辑 (temporal logic) 是一类可以通过逻辑公式精准刻画系统行为与时间相关性质的规约描述语言, 其中, 信号