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

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

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

路径过滤和
基本方法 路径过滤 路径动态选择
动态选择
迭代
系统 规约 成功率
成功 耗时 迭代 成功 耗时 迭代 过滤路径数/ 成功 耗时 迭代 次数 成功 耗时 迭代
率 (%) (s) 次数 率 (%) (s) 次数 总路径数 率 (%) (s) 次数 提升 消耗 率 (%) (s) 次数
倍数
倍数
s14 35 0.7 3 050 78 1.0 3 435 70/100 97 1.0 3 839 2.8 1.3 99 0.9 2 757
s15 35 0.6 2 666 95 0.8 2 915 70/100 100 0.8 3 143 2.9 1.2 100 0.6 2 180
s16 37 0.7 3 024 98 0.6 1 895 70/100 99 0.7 2 954 2.7 1.0 100 0.5 1 857
导航系统 s17 26 0.6 3 278 43 1.0 3 195 91/100 30 0.8 3 026 1.2 0.9 48 0.5 1 396
(2个车辆) s18 23 0.6 3 616 52 1.3 4 159 91/100 27 0.8 3 034 1.2 0.8 54 0.6 1 472
s19 38 0.7 3 510 67 1.1 4 083 70/100 81 1.7 5 325 2.1 1.5 87 1.4 4 160
s20 31 0.6 2 603 74 1.1 3 898 70/100 92 1.1 3 819 3.0 1.5 100 0.9 2 859
s21 41 0.7 2 947 99 0.6 2 153 70/100 99 0.7 2 930 2.4 1.0 100 0.6 2 029
s22 11 5.2 25 156 83 7.4 22 610 973/1 000 19 9.5 32 263 1.7 1.3 87 7.0 13 354
导航系统 s23 19 8.5 31 654 61 8.7 27 235 700/1 000 63 9.9 28 165 3.3 0.9 75 8.1 23 701
(3个车辆) s24 13 6.3 23 545 22 7.2 25 235 400/1 000 23 8.8 26 580 1.8 1.1 26 8.0 25 512
s25 4 11.9 56 162 65 10.4 24 446 973/1 000 24 10.6 31 143 6.0 0.6 71 7.6 14 918
平均 38 3.3 8 824 66 3.3 7 103 54% 75 3.2 7 660 2.5 0.9 84 2.9 5 489

RQ1: 面向规约的路径过滤算法能否有效过滤路径, 能否提升基于路径的反例生成的性能?
表 4 中的第 6–9 列为仅采用路径过滤优化后的反例生成实验数据. 其中, 第 9 列展示了 4 个系统的总路径数
以及面向每条规约可以过滤的一定不存在不安全行为的路径数目. 可以看到, 实验中的 4 个系统场景分别有 6 条、
10 条、100 条和 1 000 条系统路径. 其中, 在包含多个车辆的导航系统中, 由于组合爆炸效应, 系统总路径数较多.
根据第 9 列数据, 可以看出面向规约的路径过滤算法并不能保证在所有场景规约下都能过滤路径. 例如, 在规约
s1–s6 中, 规约与每条路径上的约束都不存在直接冲突, 因此没有路径被过滤. 然而, 在绝大多数例子中, 该算法都
检测到了可以提前过滤的路径. 该列数据显示, 在我们实验的 25 个案例中, 默认配置下的路径过滤算法平均能够
过滤一半以上 (54%) 的路径, 大幅减少了需要通过耗时的优化算法进行反例生成的路径数量.
此外, 根据第 4.2 节的实验设置, 实验中的路径过滤算法采用默认配置 (仅对布尔和线性约束进行 SMT 求解),
这可能导致部分通过非线性约束求解可被过滤的路径未被检测到. 因此, 我们进行了额外的补充实验, 评估忽略非
线性约束对路径过滤效果和效率的影响. 我们对表 4 中 25 个案例的统计显示, 算法 1 中需进行 SMT 求解的约束
里, 非线性约束占比 32%. 若在实验的路径过滤过程中, 对这部分非线性约束也进行 SMT 求解, 则平均可过滤的
路径比例可以从 54% 进一步提升至 58%, 但整体耗时也将增加至原来的 10 倍以上. 我们通过进一步分析发现, 非
线性约束求解对路径过滤有效性提升增益较小主要是因为对非线性约束进行 SMT 求解返回 UNKNOWN 结果的
概率较高, 而返回 UNSAT 结果的概率非常低. 尽管如此, 为了适应用户的系统规约与场景需求的多样性, 我们路
径过滤算法的实现上依然提供了配置选项, 允许用户自主选择是否对非线性等复杂约束进行 SMT 求解.
而从反例生成的总体性能来看, 与基础方法相比, 加上我们的路径过滤优化后, 平均成功率从 38% 提升到了
66%, 并且耗时并未因为路径过滤算法导致明显的增加. 反例生成成功率的提升主要是由于我们实验设置了对系
统进行反例生成的系统行为仿真次数上限, 即所有路径的反例生成优化算法的总迭代次数上限. 因此, 当需反例生
成的路径个数大幅减少时, 每条需进行反例生成的路径可以执行的优化迭代次数就会大幅增加.
综上所述, 实验结果表明, 面向规约的路径过滤算法能够有效过滤路径, 并提升基于路径的反例生成性能.
RQ2: 多臂老虎机算法指导的动态路径选择能否提高基于路径的反例生成的成功率和效率?
表 4 的第 10–14 列为仅采用路径动态选择优化后的反例生成实验数据. 从最后一行的平均数据来看, 加上路
径动态选择优化后, 反例生成的成功率有高达 2.5 倍的性能提升, 而找到系统不安全行为所消耗的平均迭代次数
反而下降到了原先的 0.9 倍. 在绝大多数例子里, 找到不安全行为需要的迭代次数都是下降或者几乎不变的, 而在