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

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

图测试用例, 我们选取在该论文中展示的 Nav11 地图进行实验. 该案例的地图上包含 5×5 个网格. 因此, 当地图上
有 1 个车辆时, 对应的混成自动机模型有 25 个离散节点, 车辆中有 5 个连续变量. 而当考虑 2 个车辆在地图上的
组合行为时, 对应的混成自动机模型有 25×25=625 个离散节点, 当考虑 3 个车辆在地图上的组合行为时, 对应的混
成自动机模型有 25×25×25=15625 个离散节点, 此时路径爆炸问题带来的挑战巨大.
在导航系统中, 1 个、2 个和 3 个车辆的场景下, 系统规约共有 17 条, 主要包括以下 4 大类要求.
• 车辆不进入危险网格: ¬F [t 1 ,t 2 ] (Q = q i ), 车辆避免在危险时间区间 [t 1 ,t 2 ] 进入地图上的 i 号网格;
• 车辆不进入危险区域: ¬F [t 1 ,t 2 ] (|x− x d | < l/2 ∧ |y−y d | < m/2), 车辆避免在危险时间区间 [t 1 ,t 2 ] 进入地图上以
(x d ,y d ) 为中心的, 大小为 l×m 的矩形危险区域;
)
( √
2
2
• 车辆远离危险点: G [0,60] (x− x d ) +(y−y d ) > D d , 1 h 内车辆距危险点总远于危险距离常数 D d ;
)
( √
2
2
• 车辆间防止碰撞: ¬F (x 1 − x 2 ) +(y 1 −y 2 ) ⩽ D safe , 两车距离避免小于等于安全距离常数 D safe .
我们对上述系统的 25 个系统规约进行反例生成实验. 所有实验都在同一台 PC 机上进行 (Intel Core i5-12500,
16 GB RAM, Ubuntu 22.04.4 LTS). 由于反例生成过程中使用的优化求解算法的效果具有随机性, 所以在 25 个案
例里, 每个算法都被执行了 100 次, 以对算法性能进行准确可靠的评估. 所有反例生成算法执行时, 其中的优化算
法的总迭代次数 (即系统行为的仿真模拟次数上限) 在血糖控制系统以及 1 个和 2 个车辆的导航系统中均为
10 000, 在规模和路径数目都巨大的导航系统 (3 个车辆) 中为 100 000. 此外, 在实验中, 路径过滤算法采用默认配
置, 仅对布尔和线性约束进行 SMT 求解. 路径动态选择算法中的 UCB 探索利用平衡参数 c 统一配置为常数值 1.
c 值通常能使置信区间更宽, 效果更好; 而在低维问题上较小的 值
c
尽管在实践中, 我们发现在高维问题上较大的
往往效果更佳, 但我们在实验中选择统一设置参数值, 以评估路径动态选择优化技术的通用性, 确保实验结果具有
尽可能广泛的适用性.

4.3 实验结果与分析
在 4 个系统的 25 条规约下, 反例生成实验结果见表 4, 包括使用 SNIFF 中原始的基于路径进行反例生成的基
本方法, 加上面向规约的路径过滤优化算法, 加上路径动态选择的优化算法, 以及同时加上两个优化技术扩展后的
反例生成方法的实验结果. 每种情况我们都列出了其 100 次反例生成的成功率, 成功找到不安全行为的平均耗时,
以及成功找到不安全行为的平均需要消耗的优化算法的总迭代次数 (即系统行为的仿真模拟次数).

表 4 反例生成性能比较实验结果

路径过滤和
基本方法 路径过滤 路径动态选择
动态选择
迭代
系统 规约 成功率
成功 耗时 迭代 成功 耗时 迭代 过滤路径数/ 成功 耗时 迭代 次数 成功 耗时 迭代
率 (%) (s) 次数 率 (%) (s) 次数 总路径数 率 (%) (s) 次数 提升 消耗 率 (%) (s) 次数
倍数
倍数
s1 83 5.9 6 673 74 5.7 6 374 0/6 100 2.3 2 770 1.2 0.4 100 2.0 2 310
s2 45 5.4 6 288 40 5.1 6 017 0/6 94 3.0 3 666 2.1 0.6 89 3.2 4 038
s3 21 5.2 6 228 28 6.1 6 665 0/6 70 3.5 4 471 3.3 0.7 66 3.9 5 077
血糖控制 s4 12 5.3 6 198 9 4.5 6 184 0/6 36 4.1 5 384 3.0 0.9 52 4.3 5 841
系统 s5 52 6.0 3 605 47 5.5 3 395 0/6 96 7.9 3 344 1.8 0.9 96 9.3 3 913
s6 91 5.1 3 394 92 6.0 3 724 0/6 100 4.2 1 879 1.1 0.6 100 4.3 1 953
s7 100 3.5 4 429 100 0.9 1 405 3/6 100 0.9 950 1.0 0.2 100 0.3 256
s8 79 7.7 5 864 96 6.8 3 577 3/6 97 7.0 2 991 1.2 0.5 99 6.7 2 298
s9 20 0.3 3 300 57 0.3 2 722 7/10 86 0.5 4 272 4.3 1.3 89 0.4 3 747
s10 36 0.3 3 468 81 0.4 3 358 7/10 98 0.4 3 581 2.7 1.0 99 0.3 2 584
导航系统
s11 59 0.3 3 099 93 0.2 2 060 7/10 100 0.3 2 698 1.7 0.9 100 0.2 1 844
(1个车辆)
s12 17 0.4 3 218 33 0.4 3 297 7/10 60 0.6 5 377 3.5 1.7 67 0.5 4 334
s13 26 0.4 3 630 75 0.4 3 531 7/10 93 0.4 3 907 3.6 1.1 97 0.3 2 844