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

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

true 或假 false;
• A: 表示动作 act 的有限集合, act ∈ A;
trigger,act,w
n n ∈ N trigger ∈ T act ∈ A w 为离散
• →: 表示状态迁移的有限集合, 每个迁移边表示为 n −−−−−−−→ n . 其中 , ′ , , ,
′
概率分布, 用于表示相应迁移边上的权重;
• O: 表示 ODE 等式的集合, 通过 ODE 描述车辆执行相应驾驶行为而改变自身状态的过程.

(a) 环境的元模型 (b) 交通参与者的元模型

(c) 驾驶行为的元模型
图 3 SML4ADS2.0 的元模型

基于行为规划模型的形式化语义, 为了刻画 scenario 中车辆的动态行为特性, 我们设计了 SML4ADS2.0 行为
规划模型操作语义规则, 从而支持场景树迁移边的动作迁移、无需事件触发的动作迁移以及概率动作迁移. 其中,
行为节点处执行 ODE 等式刻画物理状态的连续变化; 迁移边用来刻画车辆驾驶行为的改变. 我们定义 E n 表示以
n 的迁移边 e, trigger 条件评估取值是否为
行为节点/分支节点为源节点 T (e) 表示树形结构中迁移边 e 上的触发器
真, end n 表示当前行为节点满足状态结束条件, 如超出时限 等. 具体操作语义规则定义如下.
t
规则 1: 动作迁移.

′
((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 ′ )