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

杜德慧 等: 面向自动驾驶系统的场景建模及边缘关键场景生成 3515

关系. 场景 (scenario) 描述了一系列场面的时序关系, 每个场景都从一个初始场面开始, 通过指定动作“action”以及
目标“goals”来表征场景中的这种时序关系, 由多个场面按照时序情形依次发生的过程 [2] . 其相关定义如下.
定义 1. 场面 (scene). scene=(scenery, actors, SA, relationships, observers), 其中 scenery 表示驾驶环境, 包括静态
路网结构、静态元素、环境条件等; actors 表示交通参与者等动态元素; SA 表示动态元素的状态 (速度、位置等)
及属性; relationships 表示实体间的拓扑关系; observers 表示观察者, 能够通过传感器采集环境的状态信息.
定义 2. 场景 (scenario). scenario=(I, T, A, G), 其中 I 表示初始场面即 initial scene; T 表示场景时序关系; A 表示
智能体所有可能的行为 (actions) 集合, 例如车辆进行左变道、加速直行等; G 表示交通参与者短期与长期驾驶目
标 (goals).
定义 3. 安全关键场景 (safety-critical scenario). 安全关键场景是指高危险的具体场景, 即当场景中的危险触发
条件满足时, 可能会产生危险的场景. 通常, 此类场景跟安全相关的性质及危险触发条件相关, 是自动驾驶场景测
试的关键, 能够有效发现风险, 从而加速测试. 安全关键场景定义如下:

[ ]
ˆ θ = argmaxE x∼p θ (x) g(F, x) .
θ
场景 x 服从参数为 的分布, 安全关键场景可根据上面的公式生成. 其中 g 是度量场景风险程度及安全相关的
性质 (如碰撞率、偏离道路的距离等) 的度量函数. F 是运行在场景 x 中的自动驾驶系统, 并输出控制信号的序列.
本文的重点是如何使用形式化验证方法评估风险度量函数 g, 并生成关键场景 x.

1.2 随机混成自动机
[7]
[6]
UPPAAL-SMC 是 [5] UPPAAL 的最新扩展版本, 通过随机混成自动机 SHA 来建模具有复杂的物理行为及环
境的系统, 除支持传统的实时系统建模外, 还支持建模复杂的连续物理过程和随机行为. SHA 是自动机的一种扩
展版本, 可以定义为一个八元组: SHA=(Loc, Loc 0 , Q, Var, Inv, A, G, T). 其中,
• Loc: 表示状态的有限集合;
• Loc 0 Loc 0 ∈ Loc, 表示初始状态;
:
• Q: 表示连续变量的集合;
• Var: 表示离散变量的集合;
• Inv: 表示状态 Loc 上的不变式集合;
• A: 表示动作的有限集合;
• G: 表示迁移条件的有限集合;
• T : 表示状态迁移的有限集合. 迁移边包括迁移条件、行为动作、离散变量、连续变量和迁移概率等.
UPPAAL-SMC 能够验证系统的定性性质 P=? [F “error”], 例如, 安全性、活性、可达性等. 同时, 其验证引擎
使用了统计模型检测算法, 支持对 SHA 模型进行多种概率性质的验证, 能够定量评估系统出错的概率区间. 与传
统形式化验证方法相比, UPPAAL-SMC 无需遍历整个状态空间, 而是通过随机采样技术分析有限数量的系统仿真
运行, 从而显著降低模型检测的时间和空间复杂度, 有效地减少内存和时间开销. 具体而言, UPPAAL-SMC 将系统
的状态空间划分为两类: 可达状态和不可达状态. 对于可达状态, UPPAAL-SMC 采用蒙特卡罗抽样方法 [8] , 通过样
本分析来估计满足性质的概率; 对于不可达状态, 则通过模型检测器识别并进行剪枝, 以减少状态空间的规模. 此
外, UPPAAL-SMC 支持使用常微分方程 (ordinary differential equation, ODE) 表达式来建模时钟速率, 因此也适用
于非线性混成系统的建模.

1.3 重要性采样
重要性采样是一种蒙特卡罗积分方法, 由 Marshall 于 [9] 20 世纪 50 年代提出, 在概率密度函数难以采样或需要
采样多次的情况下, 通过选取合适的采样分布, 对原积分式进行重写, 从而提高采样的效率. 重要性采样常用于计
算较为复杂的积分, 例如高维积分、边缘分布等. 同时, 重要性采样在深度学习 [10] 、计算机视觉 [11] 、图形学 [12] 等
领域也有广泛应用, 同时它被用来估计期望值、计算复杂积分、进行贝叶斯推断等. 通过引入重要性权重, 重要性
采样能够在复杂问题中得到有效的估计结果, 提高计算的准确性和效率.