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

陈小颖 等:面向 CPS 时空性质验证的混成 AADL 建模与模型转换方法 1785

时间迁移系统的概念.
定义 5. 一个时间通信顺序进程 TCSP 的语义描述为一个时间迁移系统 TTS TCSP =〈NODES,Σ T ,→〉,NODES
为节点集合,表示各个进程.Σ T 是带延迟时间的事件集,即{(t 0 ,a 0 ),(t 1 ,a 1 ),…,(t n ,a n )},→是迁移关系,是一个三元关
(, )ta
系,→⊆NODES×Σ T ×NODES, N ⎯⎯⎯→ N ,表示 N 1 执行事件 a,延迟 t 个时间单元变成 N 2 代表的进程.
1
2
定义 6. 一个混成位置-时间迁移系统 HP-TCSP 为 HPTTS HP-TCSP =〈NODES,Σ (T,C,P) ,→〉,NODES 为节点集合,
表示各个进程.Σ (T,C,P) 是带延迟时间、条件执行以及位置赋值操作的事件集,即{(p 0 ,c 0 ,t 0 ,a 0 ),(p 1 ,c 1 ,t 1 ,a 1 ),…,
(p n ,c n ,t n ,a n )},且Σ T ⊆Σ (T,C,P) .当 p n =ε∧c n =true 时,Σ T =Σ (T,C,P) .→是迁移关系,是一个三元关系,→⊆NODES×Σ (T,C,P) ×
(, , , )pc t a
NODES, N ⎯⎯⎯⎯→ N ,表示 N 1 执行的进程进行 p 的位置赋值操作且在条件 c 满足的情况下,执行事件 a,延迟
1 2
t 个时间单元,变为 N 2 所代表的进程.
定义 7. 一个混成位置-时间通信顺序进程可以描述为一个混成位置-时间迁移系统:
HPTTS HP-TCSP =〈NODES,Σ (T,C,P) ,→〉.
2.3 HP-TCSP的操作语义

定义 8. HP-TCSP 的操作语义:
• 下面给出上面条件执行算子 Con>>P(Con:=Pf&&Place[ϕ(x)][ϕ(y)][ϕ(z)]&Pcon|true)操作语义:
v =〈 | v v ≠ pf ( )v 〉 ∨ = 〈 | x x ϕ ≠ ( )x 〉 ∨ y =〈 | y y ϕ ≠ ( )y 〉 ∨ = 〈 | z z ϕ ≠ ( )z 〉 ∨ (Pcon = false)
x
z
(2.1)
s ⎯⎯⎯⎯→ s
(, , , )pc t a
v =〈 | v v = pf ( )v 〉 ∧ = 〈 | x x ϕ = ( )x 〉 ∧ y =〈 | y y ϕ = ( )y 〉 ∧ = 〈 | z z ϕ = ( )z 〉 ∧ (Pcon = true)
x
z
(2.2)
s ⎯⎯⎯⎯→ s′
(, , , )pc t a
只有当变量 v 是按照微分方程 pf(v)变化的,并且三维坐标 x,y,z 按照ϕ(x),ϕ(y),ϕ(z)的微分方程变化,且 Pcon
为 true 时,状态 s 则在进行 p 的位置赋值操作且在条件 c 满足的情况下,执行事件 a,延迟 t 个时间单元,变为 s′
状态(2.2),否则不发生状态的迁移(2.1).
• 位置赋值算子 P Fin_Con(Fin_Con:=Fcon|true)AQ 的操作语义:
Fcon = false
(2.3)
(, , , )pc t a
s ⎯⎯⎯⎯→ s
Fcon = true
(2.4)
(, , , )pc t a
s ⎯⎯⎯⎯→ s′
只有当 Fcon 为 true 时,即中断条件满足时,才会中断当前进程,当前状态从 s 状态迁移为 s′状态(2.4);否则,
状态不发生改变(2.3).
2.4 精化关系
下面证明 TCSP 的语义模型是 HP-TCSP 的子语义模型:首先,对子语义模型进行定义;其次给出 HP-TCSP
包含 TCSP 语义的定理证明,证明 HP-TCSP 是在 TCSP 的基础上进行扩展.

定义 9. 设一个 A 类具有语义 M A 的通信顺序进程 P A 能够通过一个精化关系得到另一个 B 类具有语义 M B
的通信顺序进程 P B ,那么称语义 M B 是语义 M A 的子语义模型 [14] .P A 与 P B 的精化模型如下:
P sat S in M
B B B (P ‹ P ) .
P sat S in M B A
A A A
S A 是 P A 的语义,S B 是 P B 的语义.
定义 10. 混成位置-时间通信顺序进程 HP-TCSP 所有可接受的语言是混成位置-时间迁移序列的集合.
定理 1. 时间通信顺序进程 TCSP 的语义模型是混成位置-时间通信顺序进程 HP-TCSP 的子语义模型.
证明:令 P TCSP 是一个时间通信顺序进程.由定义 5 知,TCSP 是一个时间迁移系统 TTS TCSP =〈NODES,Σ T ,→〉
其接受的语言为 L,根据时间通信顺序进程构造一个混成位置-时间通信顺序进程,由定义 7 知,P HP-TCSP 是一个
HPTTS HP-TCSP =〈NODES,Σ (T,C,P) ,→〉.设 P HP-TCSP 能够接受的位置时间语言为 L′.此时,在 L 中任取一个时间迁移序
列 R=〈(t 0 ,a 0 ),(t 1 ,a 1 ),…,(t n−1 ,a n−1 )〉,在 L′中都有唯一一个 R′=〈(p 0 ,c 0 ,t 0 ,a 0 ),(p 1 ,c 1 ,t 1 ,a 1 ),…,(p n−1 ,c n−1 ,t n−1 ,a n−1 )〉与之对