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

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

表 1 SML4ADS2.0 场景模型到 UPPAAL-SMC 的模型转换规则

原始数据 SML4ADS2.0 UPPAAL-SMC模型
道路列表roads Road结构体
道路段列表laneSections LaneSection结构体
OpenDRIVE 车道列表lanes Lane结构体
地图数据 junctions Junction结构体
connections Connection结构体
laneLinks LaneLink结构体

节点 BehaviorName

( )
′
(n ∈ N ∧(∃E n ∧T (e) ⊨ trigger)) ⊢ n ∈ N
( )
′
∧type n ⊨ behaviorNode
trigger,act ′
n (type,t,vars,loc,o) −−−−−−−−→ n
(type ′ ,t ′ ,vars ′ ,loc ′ ,o ′ )
((n ∈ N ∧(∃E n ∧∄trigger)∧
( )
)
′
′
n ⊨ end n ) ⊢ n ∈ N ∧type n ⊨ behaviorNode
trigger,act ′
n (type,t,vars,loc,o) −−−−−−−−→ n
(type ′ ,t ′ ,vars ′ ,loc ′ ,o ′ )
行为
规划模型 状态
迁移
(( )
(n ∈ N ∧(∃E n ∧T (e) ⊨ trigger)) ⊢ n ∈ N
′
( ) ( ))
′′
′ ′ ⊢ n ∈ N
∧type n ⊨ branchPoint ∧ n ∈ N ∧∃E n ′
trigger,act,w
n (type,t,vars,loc,o) −−−−−−−−−−→ n ′′
(type ′′ ,t ′′ ,vars ′′ ,loc ′′ ,o ′′ )
车辆名称.属性 cars[index].属性
待验证 require always Expression A[] Expression
性质规约 require eventually Expression E<> Expression

算法 1 给出重要性采样生成 ADS 边缘关键场景的主要过程. 算法详细描述如下: 算法第 1 行输入是待采样的
样本数量 N, 变量 x 表示 ADS 逻辑场景的一个关键参数, p(x) 表示变量 x 满足的安全概率分布, 标记函数 g(x) 表
示变量是否满足阈值的判定函数, q(x) 表示变量 x 的提议概率分布. 算法的第 2 行输出是估计值 ˆ P (x) 和样本集
′
Dataset, 分别表示通过采样计算得到的估计值和生成的样本集. 算法的第 3 行初始化变量的值, 设置满足标记函数
cnt, 初始化为 w(x) 和采用提议分布后的新
的样本点的数量 0, 并初始化边缘关键场景集合为空, 定义重要性权重
标记函数 g(x). 算法第 4–10 行循环处理采样过程, 每次循环中首先通过 sampler 采样器对概率分布 q(x) 进行采样
′
得到一个样本 sample , 然后代入计算标记函数的值 g (x i ). 如果该值为真, 则该样本是边缘关键场景样本, 边缘关
i
键场景样本数量加 1.