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

1834 Journal of Software 软件学报 Vol.32, No.6, June 2021

+
• 时间流逝迁移:对 d∈R ,有 (, )lu ⎯⎯→ d ( ,lu + ) d ,当∀d′≤d,u 和 u+d′满足 I(l);
l u′
′
k
• 位置变化迁移:( , ) ⎯⎯→ ( , ) ,如果∃t(l,g,k,r,l′)∈T,u′=r(u),u 满足守卫 g,且 u′满足 I(l′),u 表示时间自
lu
动机中时钟的当前时间.
0
嵌入式系统通常由多个模块交互组成,因此需要引入时间自动机网 λ = λ 1 ||...|| λ n ,且 λ = (, ,L lK i , , , )V I T ,
i
i
i
i
i
i
n 是自动机的个数,这些自动机共享一组相同的动作集合.向量 l = ( ,..., )l 1 l n 是时间自动机网 λ 的位置向量.位置
′
I
约束函数 ()Il 是所有自动机λ i 约束的并集, () =∧Il ii ( )l ,其中, [/ ]ll l 表示 L 中的 l i 由 l′ 取代.
i
i
i
i
时间自动机网的语义定义为迁移系统 ()S λ =〈 S , ,s →〉 ,S=(L 1 ×…×L n )×U 是状态集合,s 0 是初始状态,→⊆S×S
0
是迁移关系,定义为:
+
• (, )lu ⎯⎯→ d ( ,lu d+ ) ,其中,d∈R ,如果∀d′≤d,u 和 u+d′满足 I(l);
′
k
• (, )lu ⎯⎯→ ( [ / ], )l l l u ,如果∃t(l i ,g,k,r, l′ )∈T,u′=r(u),u 满足守卫 g,且 u′满足 ()Il ;
i i i
, j gsync r
l′
, i gsync r
′
′
k
!, j
• (, )lu ⎯⎯→ ( [ / , / ], )l l l l l u′ ,如果存在一条边 l ⎯⎯⎯⎯→ 和另一条边 l ⎯⎯⎯⎯→ l′ ,u′=r i ∪r j (u),u
?, i
j j i i i i j j
满足守卫 g i ∧g j ,且 u′满足 ()Il ,sync 是同步信号,sync?表示接收到信号 sync,sync!表示发送信号 sync.
2.2 时间自动机模型验证工具Uppaal
[7]
Uppaal 是一个用于实时系统建模、仿真和验证的集成环境,由瑞典乌普萨拉大学和丹麦奥尔堡大学联合
开发.它适用于对带有时间的系统进行建模,并通过同步通道或共享变量实现各个时间自动机之间的通信.
Uppaal 主要由 3 部分组成:描述语言、模拟器和模型检查器.描述语言是一种具有简单数据类型(如整数、
布尔型等)的非确定性保护命令语言,可以将系统行为描述为由时钟和数据变量扩展的时间自动机网络.模拟器
是一种验证工具,它可以通过仿真检查系统可能的动态执行情况,从而在对模型进行形式化验证之前提供一种
简单的故障检测手段;而且当模型检查器检查出错误时,可以在此追溯路径.模型检查器是通过探索系统的状态
空间来检查系统的不变性和活性,即通过约束表示的符号状态进行可达性分析,从而对模型进行形式化验证.
Uppaal 中常用的数据类型包括整形(int)、布尔型(bool)、时钟(clock)和同步通道(chan),广播使用 broadcast chan
声明.
Uppaal 的主要思想是利用时间自动机来建模、仿真一个系统,优点在于高效性和便捷性.Uppaal 通过快速
搜索机制来验证系统规范和可达性,可以快速有效地对系统进行形式化验证.模型检查引擎通过 CTL 公式对系
[8]
统进行形式化验证 ,公式规则如下.
• E<>p:存在一条路径,使得 p 最终成立;
• A[]p:对所有的路径,p 一直成立;
• E[]p:存在一条路径,使得 p 一直成立;
• A<>p:对所有的路径,p 最终成立;
• p imply q:当 p 成立时,q 最终一定成立.
3 映射规则
如图 2 所示.
• A 0 是一个 Ptolemy DE 模型,A 1 ~A 3 分别是模型中的组件;
• p 0 ~p 3 是组件的输入输出接口,(p 0 ,p 1 )和(p 2 ,p 3 )分别是 A 1 和 A 2 、A 2 和 A 3 间的关系;
• T 0 是一个时间自动机网络,T 1 ~T 3 分别表示组件 A 1 ~A 3 转换生成的时间自动机;
• Temp 是时间自动机中与组件功能相同的的具体实现;
• p 01 和 p 23 分别是 T 1 和 T 2 、T 2 和 T 3 间的同步通道;
• GD 和 TD 分别表示组件接口和参数转换生成的全局变量和局部变量.
Ptolemy DE 模型转换生成一个时间自动机网络.模型中的每个组件转换成一个时间自动机,组件的接口和