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

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

为数不多的消耗的迭代次数增加的例子里, 成功率的提升都是超过 70% 的, 即提升到了原来的 1.7 倍以上. 由于我
们统计的是成功找到不安全行为时平均所需要消耗的迭代次数, 所以找到解的成功率和需要的迭代次数同时提升
的案例意味着优化后的算法在局部优化和全局优化之间取得了更好的平衡.
除此之外, 我们也尝试分析了路径动态选择技术在哪些案例上对成功率提升效果更明显. 通过具体分析我们
发现, 该技术的优化效果与被选择的路径的数目关系不明显, 与不同路径上的行为距离违背规约的程度分布差异
更相关. 譬如导航系统在 s9 的目标规约下, 有一条路径上的行为明显更容易违背规约, 而其他路径上的行为很难
违背规约, 较大的奖励分布差异使得 UCB 算法能够更快地分辨出更具有潜力的路径, 从而更多地探索该路径上的
行为空间, 更快地找到不安全行为. 此外, 像规约 s6, s7 对应的反例生成问题, 由于问题本身比较简单, 采用 SNIFF
的基本方法就已经能达到 90% 以上的成功率, 因此动态选择技术在这些案例上对成功率的提升效果比较有限, 但
此时找到不安全行为所需要的平均迭代次数大幅减少.
总之, 我们基于多臂老虎机算法指导的动态路径选择技术既减少了反例生成的耗时, 还大幅提高了基于路径
的反例生成的成功率, 性能提升非常明显.
RQ3: 当路径过滤优化和路径动态选择优化组合使用时, 我们反例生成方法的最终性能优化如何?
总体来说, 在实验的 4 个算法设置下, 我们基于路径过滤与动态选择的 CPS 系统反例生成方法的效果是最优
的, 优于 SNIFF 中的基础方法以及只加任意一种优化技术的方法. 在表 4 中, 我们将 25 个反例生成问题获得的最
高的成功率都加粗显示, 可以发现我们的基于路径过滤与动态选择的方法在 23 个例子上都有最高的成功率, 甚至
在一半以上的例子上的成功率都不少于 96%. 根据我们的实验数据, 加上两个缓解路径爆炸的优化技术后, 我们可
以将 SNIFF 基础方法的成功率提升两倍, 从平均成功率 38% 提升至 84%. 与此同时, 我们的方法也没有因为优化
技术而导致耗时增加, 反而因为需要的迭代次数减少而只需要更少的总耗时.
尽管同时加上两个优化技术后, 我们方法最终的反例生成效果优于只加任意一个优化技术的效果, 但我们也
发现两个优化技术同时使用对反例生成效果的提升要少于两者单独使用效果提升的总和. 譬如在基本方法上加入
路径过滤优化后成功率平均提升了 28% (从 38% 到 66%), 但在已经进行了路径动态选择优化后的算法上再加入
路径过滤优化, 成功率仅提升了 9% (从 75% 到 84%). 我们认为这主要是因为路径过滤和路径动态选择这两种优
化技术本质都在试图解决类似的问题, 即通过减少分配 (或不分配) 给不具有潜力的路径探索状态空间的计算资
源来缓解路径爆炸问题. 因此, 两种优化技术对反例生成性能增益部分有所重叠, 从而减少了总体的额外增益. 但
两者评估路径潜力的方法角度不同: 路径过滤采用的是 SMT 技术验证路径上的部分约束与目标规约之间的约束
满足关系, 而路径动态选择是对不同路径上行为的奖励分布进行区分, 前者在存在简单直接的约束冲突时表现更
好 (譬如表 4 中的规约 s18, s22), 而后者在奖励分布差异较大时表现更好. 因此, 两个优化技术叠加使用可以最大
化地缓解路径爆炸问题, 以确保最终能够尽可能地达到最佳的反例生成性能和效果.

5 结论及未来工作

本文提出了一种基于混成自动机路径过滤和动态选择的 CPS 系统反例生成方法, 以应对系统反例生成过程
中的路径爆炸问题. 首先, 我们提出了面向规约的路径过滤方法, 通过分析系统规约的语法树及系统路径上的行为
约束, 快速过滤不可能包含不安全行为的路径, 从而有效减少需要探索的路径数量. 其次, 我们引入了多臂老虎机
算法, 用于指导反例生成过程中的路径动态选择, 根据已探索路径的信息动态调整计算资源的分配, 尽可能将资源
分配给更有潜力的路径, 最大化反例生成的性能和效率. 实验结果表明, 本文方法显著提升了 CPS 系统反例生成
的性能, 将成功率提高了两倍以上.
由于本文方法是基于混成自动机上的路径的, 故面向的是具备混成自动机模型的 CPS 系统, 或者至少需具备
系统的路径结构信息. 然而, 混成自动机等形式化模型在工业界的应用仍较为有限, 复杂 CPS 系统的混成自动机
模型往往难以获取. 目前, 已有一些研究关注如何自动从系统的 Simulink 模型转换获取混成自动机模型 [39] , 或从
系统的时序轨迹中学习生成混成自动机等形式化模型 [40–44] . 因此, 当无法获取 CPS 系统的形式化模型时, 可以先