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

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

的随机行为. 而 UPPAAL-SMC 使用随机混成自动机模型支持随机混成行为的验证分析, 且具有较强的定量性能
分析能力, 能够较好地反映出自动驾驶汽车的相对安全性. SML4ADS2.0 场景模型采用 JSON 作为数据交换的格
式. 因此实现 SML4ADS2.0 到 UPPAAL-SMC 模型的转换首先需要对 JSON 格式的 SML4ADS2.0 场景模型实例
按照具体的语法关键字进行解析, 得到原始数据信息. 这些数据信息主要包括 OpenDRIVE 地图、车辆信息、车
辆行为规划模型以及待验证的性质规约字符串. 如图 6 所示, 将这些 SML4ADS2.0 场景模型中的原始数据转换到
UPPAAL-SMC 所支持的数据可以划分为以下 3 个部分.
1) OpenDRIVE 地图文件、天气以及车辆属性等静态场景元素的转换. 由于 UPPAAL-SMC 无法直接解析描
述地图信息的 OpenDRIVE, 因此, 需要对 SML4ADS2.0 场景模型文件中引用的 OpenDRIVE 地图文件进行解析,
将路网的各个组成部分通过事先预定义的数据结构声明模板转化为 UPPAAL-SMC 中可读的数据类型, 从而支
持路网信息的描述. 但是 UPPAAL-SMC 中支持的数据结构有限, 转换过程中需要对相关数据进行一定的抽象
处理.
2) 车辆行为规划模型到 SHA 自动机网络的转换. UPPAAL-SMC 借助随机混成自动机网络建模复杂系统的
行为. 因此, 本文将一个车辆的树结构行为规划模型转化为一个混成自动机模型, 并根据场景模型中表示执行周期
的 timeStep 属性, 构建了控制执行周期的自动机, 从而形成随机混成自动机的网络, 建模单位时间步长内 Ego 车
移动的过程.
3) 待验证的性质规约的转换. 根据 SML4ADS2.0 关于车辆待验证性质规约的具体语法形式, 可以将其转
化为 UPPAAL-SMC 中支持的时态逻辑表达式, 从而利用 UPPAAL-SMC 工具对转化后的场景模型进行验证
分析.

SML4ADS2.0 到 UPPAAL-SMC
模型的转换 UPPAAL-
SMC 中支持的
地图组成 数据结构
输入 文 车辆属性 输出
件 功能函数
解
析 行为规划模型 自动机网络
JSON 格式的场景 XML 格式的 UPPAAL
模型实例文件 SMC 模型实例文件
待验证性质 性质规约
图 6 SML4ADS2.0 到 UPPAAL-SMC 的自动转换

接下来如后文表 1, 针对 SML4ADS2.0 场景模型的模型转换设计具体模型转换规则. 包括静态数据的转换和
车辆行为规划模型到 SHA 网络的转换, 以及部分在 UPPAAL-SMC 模型中需要使用的重要功能函数.
基于 SHA 的语义模型, 本文设计、实现了 SML4ADS2.0 的自动转换规则及算法实现, 具体实现细节请参见
文献 [18], 当用户构建场景模型后, 可以自动实现场景模型到验证模型 SHA 的转换, 进而使用 UPPAAL-SMC 对
场景模型进行验证分析.

3.2 基于重要性采样的边缘关键场景生成
本文针对边缘关键具体场景的生成问题, 提出基于重要性采样的边缘关键场景生成方法, 本质上是根据 UPPAAL-
SMC 验证分析的结果, 获取关键参数域与概率分布 p(x), 得到 ADS 安全关键逻辑场景. 根据概率分布特性, 通过
传统蒙特卡罗均匀采样对逻辑场景的参数范围均匀地随机选点, 不仅很多样本会落在对计算结果贡献不大的区
域, 而且通过蒙特卡罗均匀采样虽然能得到大量的具体场景, 但是样本数量仍然非常大, 其中包含大量非安全关键
的场景. 因此, 本节基于重要性采样方法, 通过设计一个风险事件发生概率更高的混合高斯提议分布代替原有的分
布, 引入重要性权重函数 w(x) 减少两个分布的方差, 从而获得边缘关键具体场景 [19] .