Page 259 - 《软件学报》2021年第6期

陆芝浩 等:Ptolemy 离散事件模型形式化验证方法 1833

当事件队列为空时,说明模型的一次执行结束.
算法 1. Semantics of Ptolemy Discrete Event Model.
1: Q:=∅;
2: for each actor A in model do
3: Ainit(⋅)
4: end for
5: while Q is not empty do
6: event:=head event of Q
7: remove event from Q
8: actorToFire:=getActorByEvent(event)
9: actorToFire.prefire(⋅)
10: actorToFire.fire(⋅)
11: actorToFire.postfire(⋅)
13: end while
在 DE 模型中,消息通过组件之间的连接进行瞬时传递,模型中时间的推移是通过时钟组件实现的.DE 模型
按照时间顺序进行执行,首先执行时间最早的事件(拥有最早的时间戳).随着事件的处理,在模型内和外部世界
的时间都会向前推移,因此逻辑时间和物理时间之间会产生混淆.逻辑时间是模型中的时间,物理时间是模型执
行时现实世界中消耗的时间.逻辑时间可能会比物理时间走的更快或更慢.
DE 控制器中的 synchronizeToRealTime 参数设置为 true 时,可以在某种程度上让这两个时间同步,它通过延
缓模型的执行以便物理时间追上逻辑时间.当然,这只有在计算机足够快地执行这个模型使得逻辑时间远远快
于物理时间的情况下才起作用.当这个参数设置为 true 时,逻辑时间值以秒为单位,否则时间单位是任意的.

2 时间自动机模型

[5]
时间自动机 是在传统自动机上进行实时扩展.设 V 是有限变量集合,C 是有限时钟变量集合,X 是有限数据
变量集合,有 V=C∪X 且 C∩X=∅.所有的时钟变量同步向前演进.我们用ψ(V)表示位置约束和守卫函数的集合,
有ψ::=e|ψ∩ψ,e 是形如 c~n 或者 x~n 的表达式,其中,c∈C,x∈X,~∈{≤,≥,=,<,>}.赋值操作定义为 v:=e,v∈V.我们
用 U 表示所有的赋值函数.

2.1 时间自动机语义
时间自动机是一个六元组λ(L,l 0 ,K,V,I,T),其中,
• L:有限的位置集合;
• l 0 :初始位置;
• K:有限的动作集合;
• V:有限的变量集合;
• I:L→ψ(V)是位置约束函数;
• T:T⊆L×ψ×K×U×L 是有限的边的集合.
每条边有一个源位置 l、一个目标位置 l′.当边上的守卫 g∈ψ满足时,迁移发生并且变量集 V 中的部分变量
通过函数 r∈U 更新.边 t〈l,g,k,r,l′〉常写作 l ⎯⎯⎯→ . l′
gk
,,r
自动机初始状态位于初始位置 l 0 ,且所有时钟变量初始化为 0.随着时间流逝,所有的时钟变量按照相同的
频率增长,且满足位置约束 I(l 0 ).当该位置上的变量满足边上的使能守卫 g 时,系统可以继续停留在这个位置或
[6]
者迁移到位置 l′.当动作 k 发生时,变量根据函数 r 的定义发生改变 .
时间自动机λ(L,l 0 ,K,V,I,T)的语义定义为一个标号变迁系统 S(λ)=〈S,s 0 ,→〉.S⊆L×U 是状态的集合,s 0 是初始
状态,→⊆S×(U∪K)×S 是迁移的集合,分为两类.