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

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

参数分别转换成时间自动机中的全局变量和局部变量,组件间的关系转换成一组同步通道,实现各个时间自动
机间可以通过同步通道通信,从而构成一个时间自动机网络.其中,由于 Ptolemy DE 模型与时间自动机模型在复
杂数据类型(如 double、矩阵)和复杂计算(如三角函数、指对数函数)方面的支持力度不同,所以本文中的方法
暂未涉及对这些复杂数据类型和复杂计算的转换规则.

D 1: DE director A 0: DE system

p 0 p 1 p 2 p 3
A 1 A 2 A 3

T 0: Uppaal system
T 1 T 2 T 3
Temp Temp Temp
p 01! p 23!
s 0 s 1 s 0 s 1 s 0 s 1
p 01? p 23?
GD port LD para GD port LD para GD port LD para

Fig.2 Visual rendition of the map of ptolemy DE model to network of automata
图 2 Ptolemy DE 模型到时间自动机网络的映射关系示意图

Ptolemy DE 模型本质上是一个复合组件 A=(E,∅,Para,R),其映射规则如下:
Translate () A ≅ Trans _ Actors E ∩ ( ) Trans _ Paras (Para ∩ ) Trans _ Relas R
( )
( ) Trans Actor E≅
Trans _ Actors E _ ( [1]) ∩ ...∩ Trans _ Actor E x
( [ ])
[ ])
Trans _ Paras (Para ) Trans Para≅ _ (Para [1]) ∩ ...∩ Trans _ Para (Para y
( ) Trans Re≅
...
Trans _ Relas R _ la ([1])R ∩∩ Trans _ Rela ( [ ])R z
参数 x表示 A中的组件个数,y 表示 A中的参数个数,z表示 A中的关系个数,E[i],Para[i],R[i]分别表示 E,Para,
R 中的元素.Ptolemy DE 系统的转换包括组件集合 E 的转换、参数集合 Para 的转换和系统中组件间关系 R 的
转换.Ptolemy DE 系统最终被转换成一个等价的时间自动机网络.
3.1 数据类型
Ptolemy 支持丰富的数据类型,但是时间自动机却并非如此.为了将 Ptolemy DE 模型转换为等价的时间自
动机模型,设计对 Ptolemy 中数据类型的转换显得尤为重要.本文提出:
(1) 将 Ptolemy 中 int 和 bool 类型的数据直接转换为时间自动机中 int 和 bool 类型的数据;
(2) Ptolemy DE 模型中的时间组件具有 period 和 offsets 两个参数:period 表示周期,offsets 表示偏移量,是
一个长度为 n 的数组(offsets[i]<offsets[j]<period,i<j<n).时间组件在 time 时刻触发,time=b×period+
offsets[i](b∈N).为了保证时间自动机也表达这一特征,除转换参数 period,offsets 和 time 的计算外,还需
为其定义一个局部时钟变量 t,并将 Edge(l,g,k,r,l′)中 l 状态的 invariant设置为 t≤time,g 设置为 g≥time,
此时即可满足时间自动机在 time 时刻才能发生迁移.k 表示和其他的时间自动机交互通信,r 用于完成
对输入和输出接口、参数及 b 和 i 的赋值修改操作.

3.2 关系
两个内部组件的端口或一个组件的端口与一个组件的内部组件的端口之间的关系 R=(p,Para,q):
Trans _ Rela ()R ≅ Trans _ ROP ( )p ∩ Trans _ RIP ( )q
Trans _ ROP ( )p ≅ Edge a ( , , !, , )l φ p r l′ a
a
a
Trans _ RIP ( )q ≅ Edge b ( , , ?, , )l φ p r l′ b
b
b
R 是连接组件 A 的输出端口 p 与组件 B 的输入端口 q 的关系,对应转换成一组同步迁移.Edge a (l a ,∅,p!,r a , l′ )
a