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

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

(第 15 行). 该算法通过多臂老虎机问题的 UCB 算法, 尽可能地平衡对不同路径下系统的行为空间的探索和利用,
自适应地动态调整对不同路径的反例生成的资源分配, 从而提高了反例生成的性能.

4 实验分析

4.1 工具实现
本文提出的路径过滤与动态选择算法可以普遍适用于基于路径的 CPS 系统反例生成中. 正如在本文相关工
作章节中所讨论的, 现有的基于路径的 CPS 系统反例生成工具主要包括 PDF [13] 和 SNIFF [14] . 其中, PDF 仅支持对
系统的可达性规约 (reachability property) 进行反例生成, 而 SNIFF 则支持更加广泛的信号时序逻辑规约. 鉴于本
文方法同样可以支持表达能力更强的信号时序逻辑规约, 我们将本文方法在工具 SNIFF 的基础上采用 C++进行
了扩展实现.
具体来说, 在面向目标规约的路径过滤算法实现中, 我们采用了较为成熟的 Z3 [36] 求解器进行 SMT 约束求解.
并且, 路径过滤算法的实现为用户提供了参数选项, 支持用户选择针对布尔、线性、非线性等类型的约束进行基
于 SMT 求解的路径过滤检查 (默认参数设置为仅检查布尔和线性约束). 此外, 动态路径选择算法的实现也为用户
提供了参数选项, 支持用户对 UCB 算法中平衡空间探索与利用的参数 c 进行设置 (默认值为 1).

4.2 实验设置
为了评估基于路径过滤和动态选择的 CPS 系统反例生成方法的有效性, 我们研究了以下 3 个问题.
• RQ1: 面向规约的路径过滤算法能否有效过滤路径, 能否优化基于路径的反例生成的性能?
• RQ2: 多臂老虎机算法指导的动态路径选择能否提高基于路径的反例生成的成功率和效率?
• RQ3: 当路径过滤优化和路径动态选择优化组合使用时, 我们反例生成方法的最终性能优化如何?
为了实验评估上述问题, 我们将工具 SNIFF 以及我们扩展后的不同版本, 分别应用在一组经典的混成系统反
例生成的测试用例上. 这组测试用例中的系统均规模较大或具有复杂的非线性行为. 表 3 中列出了涉及的每个系
统的名称, 系统对应的混成自动机模型上的连续变量数, 离散节点数, 离散跳转数等信息, 最后一列还标出了从自
动机模型的初始节点出发到达目标节点的有界路径的数目, 路径数在 6–1 000 条不等.

表 3 测试用例系统的混成自动机模型信息

系统 连续变量数 离散节点数 跳转数 初始节点 目标节点 路径数目
血糖控制系统 4 6 10 q 1 q 5 6
导航系统 (1个车辆) 5 25 80 q 2 q 19 10
导航系统 (2个车辆) 10 625 160 (q 2 ,q 2 ) (q 19 ,q 19 ) 100
导航系统 (3个车辆) 15 15 625 240 (q 2 ,q 2 ,q 2 ) (q 19 ,q 19 ,q 19 ) 1 000

表 3 中, 血糖控制系统 [37] 模拟了糖尿病患者的人体血液系统中葡萄糖与胰岛素相互作用的动力学模型, 考虑
了胰岛素注射和碳水化合物摄入对血糖水平的影响. 具体而言, G 为高于基础值 G B 的血浆葡萄糖浓度, 为高于基
I
础值 I B 的血浆胰岛素浓度, X 为间质室中的胰岛素浓度, 其行为可根据胰岛素注射策略以及碳水化合物摄入后的
时间划分成 6 个不同的模式 (离散节点), 每个模式下其连续行为都由非线性的多项式模拟.
在糖尿病患者的血糖控制系统中, 系统规约共有 8 条, 主要包括以下 3 大类要求.
• 避免严重高血糖: G [0,360] (G < G serveHyper ), 6 h 内血浆中的葡萄糖浓度总低于浓度上限 G serveHyper ;
• 避免长期较高血糖: ¬F (G [0,120] (G > G hyper )), 血糖浓度避免连续 2 h 都高于高血糖浓度常数 G hyper ;
• 避免长期低血糖: ¬F (G [0,20] (G < G hypro )), 血糖浓度避免连续 20 min 都低于低血糖浓度常数 G hypro .
导航系统 [20,38] 模拟移动实体 (例如车辆) 在一个网格化的二维地图内移动的动态行为. 地图里包含实体的初始
v d , 实体的实
网格, 要到达的目标网格, 以及需要避免的不安全网格. 实体在每个网格下都有一个特定的期望速度
际速度由微分方程 ˙ v = A(v−v d ) 确定, 其中 A 是一个矩阵, 保证速度收敛到期望速度. 文献 [38] 中提供了一系列地