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

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

Pgrn 和 Cgrn 分别是定义的表示行人交通灯绿灯和车辆交通灯绿灯亮灭的参数.当该属性满足时,证明系统
不存在车辆交通灯和行人交通灯同时为绿的情况.
(3) A[⋅](Decision.AbNormal imply!TrafficLight.normal)
AbNormal 是异常生成器 Decision 中表示出现异常的状态,当系统出现异常时,交通灯控制器 TrafficLight
不能处于 normal 状态.如果该属性满足,则证明当系统出现异常时,交通灯控制器 TrafficLight 处于异常状态.
(4) A[⋅](Decision.AbNormal imply(Pgrn==0 and Pred==0 and Cgrn==0 and Cred==0 and (Cyel==0 or
Cyel==1)))
Decision 处于 AbNormal 状态时,表示系统出现异常,此时,Pgrn,Pred,Cgrn 和 Cred 的值都为 0,Cyel 的值在 0
和 1 之间交替变换.如果该属性满足,则证明当系统出现异常时,只有指示车辆暂停行动的黄灯闪烁,其他灯灭.
(5) A[⋅] not deadlock
该属性验证公式用于验证系统中是否存在死锁.
表 1 是上述验证公式详细的验证情况,当时间自动机模型中有不满足的属性时,Uppaal 验证引擎可以返回
异常路径.
Table 1 Details of verifying formulas
表 1 属性公式验证消耗
验证公式 验证费时(s) Kernel 费时(s) 总费时(s) 常驻内存(KB) 虚拟内存的使用峰值(KB) 验证结果
(1) 0 0 0.003 6 804 26 228 满足
(2) 0 0 0.004 6 892 26 216 满足
(3) 0 0 0.042 6 930 271 251 满足
(4) 0 0 0.045 7 012 280 134 满足
(5) 81.62 0.218 82.751 137 340 284 156 满足
6 相关工作

在模型驱动开发过程中,模型从各个角度对系统进行了描述 [10] ,是早期对可靠性进行分析的一个重要环节.
然而,工业界建模工具中的模型通常缺乏形式语义,无法进行形式验证,所以研究人员采用模型转换的思想 [11,12] ,
在保证语义一致的基础上,将构建好的模型转换为可以进行验证的形式化模型,如将 UML,AADL,Yakindu
statecharts,POOSL,TASM 或者 Simulink 构建的模型转换为一种形式化模型,进而实现验证.北京大学的研究团
队提出了 UML 到 Markov 链的语义转换,通过在 UML 的用况图、活动图、顺序图、构件图中加入可靠性相关
的信息,构造出整个系统的构件转移图;根据系统的构件转移图,并结合构件图中描述的单个构件的可靠性,最
终构造出用于可靠性分析的 Markov 链 [13] .空中客车公司的 TOPCASED 项目提出了 AADL [14] 到中间语言 Fiacre
的语义转换,主要给出了线程执行和通信的转换原理,所关注的研究子集和转换规则采用自然语言进行描述 [15] .
法国 IRIT 实验室采用动作时序逻辑描述语言 TLA+对 AADL 执行模型的部分语义做了初步研究,包括端口通
信、共享变量的构件间通信、抢占式调度策略以及模式的语义.这是 AADL 语义形式化的最早研究工作,其转
换规则主要以语义函数的方式给出,但 TLA+的模型检测工具 TLC 的验证能力较弱 [16] .伊利诺斯理工大学的研
[9]
究团队提出了 Yakindu statecharts 到时间自动机模型的相关转换、验证工作 ,并给出了判断转换前后模型一致
性的条件以及验证属性不满足时追溯原模型中路径的方法;该团队还提出了将 Stateflow 模型转换为时间自动
机模型,进而使用 Uppaal 进行验证的方法 [17] .特文特大学的研究团队提出了一种将简化了的运动控制系统的
[8]
POOSL 模型转换为时间自动机模型的方法 ,并验证了其功能行为和最坏情况下的延迟.北京航空航天大学的
研究团队给出了 TASM 到时间自动机模型地转换语义,并开发了一个自动转换工具 [18] ,通过 atlas 转换语言,将
TASM 转换为时间自动机模型,进而进行相关的形式化验证工作.以色列的某研究团队设计了一个转换验证工
具 TVS,将 Simulink 模型转换成优化的 C 代码 [19] ,并重点介绍各种技术问题,比如特征不变量的自动生成.中国
科学院软件研究所的研究团队提出了将 Simulink/Stateflow 图形模型转换成 HCSP 形式模型的方法,并使用
HHL 及其定理证明器形式化验证了转换后的形式模型 [20] .清华大学的研究团队提供了使用时间自动机描述和
验证多时钟系统的方法 [21,22] .