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

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

Fig.12 Automaton of PedestrianLightNormal
图 12 PedestrianLightNormal 时间自动机

图 13 是由 TrafficLight error 细化模型转换而来并进行优化的时间自动机,不必为输出接口产生同步信号.
每组迁移首先 TrafficLight_error_down?接收顶层传来的同步,然后判断迁移的约束条件是否满足:若满足,则对
输出接口进行赋值并修改参数,更新到目的状态,同时产生同步信号 TrafficLight_error_sync!与顶层同步;若不满
足,则返回迁移的源状态,同时产生同步信号 TrafficLight_error_sync!与顶层同步.时间自动机中除初始状态外,
每个状态也都对应有一条以初始状态为目标状态的迁移 TrafficLight_error_init?,用于初始化时间自动机.

Fig.13 Automaton of refinement of TrafficLight error
图 13 TrafficLight error 细化模型的时间自动机

5.4 属性验证
在此基础上,通过提取 Ptolemy DE 模型中的属性特征,形式化描述为 CTL 公式,进而使用 Uppaal 验证的引
擎对模型的可靠性、安全性、死锁进行形式化验证.
(1) A[⋅]!(CarLightNormal.Cgrn && PedestrianLightNormal.Pgrn)
Cgrn 和 Pgrn 分别是车辆交通灯控制器 CarLightNormal 和行人交通灯控制器 PedestrianLightNormal 中表
示对应绿灯亮的状态.如果该属性满足,则证明系统不存在车辆交通灯和行人交通灯同时绿灯亮的情况.
(2) A[⋅]!(Pgrn==1 and Cgrn==1)