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

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

的分析提供了统一的语义基础. 相比于已有的工作, 本文方法有助于自动驾驶场景建模并提供了丰富的动态行为
语义模型, 为场景模型的测试、验证奠定了基础.

3 基于 UPPAAL-SMC 的逻辑场景验证分析及边缘关键场景生成

本节重点讨论在边缘关键场景的生成方面, 根据场景验证分析的结果, 得到安全关键的逻辑场景模型, 针对场
景中关键参数与概率分布, 使用基于重要性取样的场景生成方法, 得到边缘关键的具体场景. 本文提出的边缘关键
场景生成方法, 结合了基于 UPPAAL-SMC 的逻辑场景验证分析的优点, 能够高效地对场景的抽象状态空间进行
搜索并对系统满足性质约束的概率区间进行评估, 能够评估场景中风险发生的概率区间, 进而锁定关键场景. 同
时, 结合基于重要性采样的方法有效生成边缘关键具体场景.
基于重要性采样的边缘关键场景生成步骤如图 5 所示, 首先使用场景建模语言 SML4ADS2.0 构建逻辑场景
模型并根据场景需求设计场景中关键参数的输入范围. 然后, 使用 UPPAAL-SMC 验证分析场景模型是否满足给
定的性质约束, 以确定场景安全程度, 进而可以根据量化分析的结果评估、确定关键参数的取值范围; 最终输出的
是调整后的参数范围, 也就是被认为更容易造成风险场景的关键参数域及其概率分布. 一旦确定了关键参数域及
其概率分布, 使用重要性采样进行加速采样, 找出不易发生的安全关键场景. 原始的场景概率分布不均, 边缘的安
全关键场景不容易生成, 通过新的提议分布替换概率分布, 从而提高边缘关键场景的发生概率. 根据提议概率分

布, 通过标记函数 g(x) 判断其是否为边缘关键场景, 如果是, 则将该边缘关键场景保存在场景数据库中. 记录好一
个安全攸关具体场景后, 判断是否完成迭代, 是的话便结束整个流程. 迭代的判断依据是生成的待采样本集合. 该
流程中的关键步骤是基于 UPPAAL-SMC 的逻辑场景验证分析与基于重要性采样的边缘关键场景生成, 从而实现
逻辑场景到边缘关键具体场景的生成.

SML4ADS2.0 基于 UPPAAL-SMC
场景建模 的性质验证
SML4ADS2.0
场景建模语言 模型转换
安全关键
逻辑场景模型

基于重要性采 关键参数域
样的场景生成 与概率分布

待采样本集
否
是
标记函数
g(x) 判定

是

保存边缘 是否继续
关键场景 迭代
否
图 5 基于重要性采样的边缘关键场景生成

3.1 基于 UPPAAL-SMC 的逻辑场景验证分析
SML4ADS2.0 通过初始位置的概率分布设置以及树结构行为规划模型的分支特性, 从而支持建模场景中车辆