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

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

5 案例分析

5.1 情景描述
如图 5 是一个交通信号灯系统,指示车辆行动的信号灯有红、黄、绿这 3 种,指示行人行动的指示灯有红、
绿这两种.当系统正常工作时:
汽车指示灯按照红、黄、绿、黄的顺序变换,分别停留 3,1,2,1 个时间单元;
行人指示灯根据汽车指示灯的变换而变换:当汽车指示灯由红变黄时,行人指示灯变红;当汽车指示灯由黄
变红时,行人指示灯变绿.
有时系统会出现故障,此时只有指示汽车暂停行驶的黄灯闪烁,其他指示灯都灭.特殊情况包括:(1) 车辆和
行人不能同时行动,即两种指示灯不能同时为绿色;(2) 当信号灯系统出现故障时,只有黄灯闪烁,其他灯不亮.

Fig.5 Traffic environment
图 5 交通灯系统实体图

5.2 Ptolemy DE模型
如图 6,Ptolemy DE 模型中定义了 5 个参数:Pred,Pgrn,Cred,Cyel 和 Cgrn,分别表示不同的交通灯:当值为 1
时,表示其对应的交通灯亮;值为 0 时,表示其对应的交通灯灭.如图中参数 Pred 和 Cyel 值为 1,则行人红灯和车
辆黄灯亮.DiscreteClock 是一个事件源组件,以 1 为周期产生输出信号,Decision 是一个异常生成器,TrafficLight
是交通灯控制器,SetVariable 组件用于更新参数值.
组件 Decision 是一个有限状态机,功能是模拟系统中产生异常,其中包含 Normal,Abnormal 两个状态和一个
number 参数.Decision 在状态 Normal 上停留 15 个时间单元,每个时间单元,Ok 接口都会产生输出表示系统正常;
之后,Error 接口产生输出表示系统出现异常,Decision 更新到 Abnormal 状态.在状态 Abnormal 上停留 5 个时间
单元,每个时间单元,Error 接口都会产生输出表示系统出现异常;之后,Ok 接口产生输出表示系统恢复正常,
Decision 更新到 Normal 状态.Decision 负责维持系统 15 个时间单元正常、5 个时间单元异常,依次交替更新.
组件 TrafficLight 交通灯控制器是一个模态模型,有两个状态 normal 和 error,状态 normal 和 error 各有一个
细化模型.TrafficLight 处于状态 normal 时表示系统正常,可以正常控制交通灯;处于状态 error 时表示系统出现
异常,控制交通灯显示异常情况,只有黄灯闪烁,其他灯都不亮.TrafficLight 处于 normal 状态,当输入接口 Error
有输入信号时,表示系统出现异常,TrafficLight 更新到 error 状态,同时初始化 error 状态中的细化模型;
TrafficLight 处于 error 状态,当输入接口 Ok 有输入信号时,表示系统恢复正常,TrafficLight 更新到 normal 状态,
同时初始化 normal 状态中的细化模型.