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

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

速、10% 的概率减速且目标速度是 12、40% 的概率加速, 且目标速度是 20. 通过这种图形化的建模方式, 为设计
者定义车的行为轨迹提供了方便. 超车场景具体实验细节参见: https://github.com/Term-inator/SML4ADS, 此外, 其
他场景建模的案例也可参见该链接.

(a) Ego 车行为规划模型 (b) F2 车行为规划模型
图 8 变道超车场景中车的树形结构行为规划模型

根据我们提出的 SML4ADS2.0 到 SHA 的模型转换方法, 可以得到变道超车场景的 SHA 模型如后文图 9 所
示. 这些 SHA 模型准确建模了场景中关键组件的动态行为, 其中, Ego 车的行为最为复杂, 需要根据周边环境的变
化, 执行不同的动作. 图 9(d) 为 Ego 车的 SHA 模型.

4.2 边缘关键场景生成
该案例的自动机网络模型及其需要满足的度量区间逻辑 (metric interval temporal logic, MITL) 性质规约, 可使
用 UPPAAL-SMC 工具进行形式化验证分析. 本文从 Ego 车的角度, 验证、分析了关于 Ego 车是否超车成功的相
关性质规约, 如下.
1) 性质 1: Pr[<=400;200] ([] (cars[0].laneId == cars[1].laneId && alltime > 0) imply (cars[0].offset – cars[1].offset
>= 20 + 1.5 × cars[1].speed)).
该性质规约用于评估在 400 个时间单位内, 对系统进行 200 次仿真实验, 当 Ego 车与 B1 车在同一条车道时, Ego
车与 B1 车是否能够一直满足安全距离. UPPAAL-SMC 评估系统模型满足该性质规约的概率区间为 [0.302 97,
0.440 946], 表明该场景下两车距离满足安全距离的概率区间较小, 即两车相撞的概率较大, 因此, 该场景属于安全
关键场景.
2) 性质 2: Pr[<=400;200] ([] (cars[0].laneId == cars[1].laneId && alltime > 0 && cars[0].offset > cars[1].offset)

imply (cars[0].offset – cars[1].offset >= 20 + 1.5 × cars[1].speed)).
cars[0].offset > cars[1].offset, 表示 Ego 车的纵向偏移距离大于 B1 的纵
该性质规约增加了一个前提条件约束
向偏移, 此时能够满足两车最大安全距离约束的概率区间为 [0.605 346, 0.739 374], 在 Ego 车变道的过程中, B1 车
还在向前行驶, 因此可能会存在 Ego 车变道时满足安全距离公式, 但是变道到 lane1 时, B1 车向前行驶, 可能会导
致 Ego 车变道完成后与 B1 的距离小于安全距离公式. 通过分析该性质规约, 我们发现如果要确保两车保持安全
距离的概率大于 0.6, 需要特别关注 Ego 车与被超车辆之间的距离. 通过这种量化分析、评估方法, 影响 ADS 场景