图4.30  进路延时解锁流程图
4.5.2    延时解锁模型
 
图4.31  进路延时解锁的时间自动机模型
延时解锁是一种非正常解锁，当列车车已经接近并且进路处于接近锁闭时所采取的特殊措施。在这里需要ATS模块来启动该模块，它会发出一个命令，延时解锁模块收到命令后，判断该命令如果有效则立即关闭信号机，并开始计时，延时30秒后自动解锁进路，延时解锁的时间自动机模型如图4.31所示。
表4.6  进路延时解锁模型主要位置、通道说明表
位置集合    通道集合
主要位置    说明    通道    说明
Idle    初始位置    TimeUnlockApp    延时解锁命令
ComdDeal    延时命令接收    UnlockReply    命令应答
check    命令有效性检查    CloseSignal    关闭信号机命令
InvalidComm    无效的命令    CloseOver    信号机已关闭
CondiFill    命令有效        
DelayWait    延时等待解锁        
TunlockOver    延时解锁完成        
时钟clock_TU主要用来判断延时的时间是否到达，这里我们设置延时的时间为30秒。TimeUnlockApp为ATS发来的命令，收到后回复一个UnlockReply命令。变量SigStatus表示信号机开放还是关闭，变量Train表示是否有列车占用，变量Routestatus表示进路状态。
4.5.3    延时解锁模拟仿真
   
图4.32  延时解锁的消息序列
在信号控制模块SignalHold位置，由于ManualUnlock人工解锁等于1，进路状态routestatus=4，ATS模块会发出一个TimeUnlockApp延时解锁命令，延时解锁模块收到这个命令后启动计时器clock_TU开始计时，并来到ComdDeal位置，然后回复一个UnlockReply命令给ATS。到了Check位置，此时判定，进路状态routestatus为4，并且信号处于开放状态SigStatus=1，并且没有列车Train=0，判定符合后到CondiFill位置，发送CloseSignal命令给信号控制模块，信号控制模块将信号机关闭，关闭后会发送一个CloseOver命令给延时解锁模块，收到这个命令后将clock_TU计时器清零，并开始计时，来到DelayWait位置，等过了30秒后，表示延时结束，将计时器清零，并将进路状态routestatus置0，表示经过30秒后自动解锁，最后延时解锁结束，到了TunlockOver位置，最后回到初始位置。
 
图4.33  进路无效延时解锁的消息序列
图4.33为进路延时解锁无效命令的消息序列。在信号控制模块SignalHold位置，由于ManualUnlock人工解锁等于1，进路状态routestatus=4，ATS模块会发出一个TimeUnlockApp延时解锁命令，延时解锁模块收到这个命令后启动计时器clock_TU开始计时，并来到ComdDeal位置，然后回复一个UnlockReply命令给ATS。到了Check位置，此时判定，当有列车Train=1，或者进路状态routestatus不等于4，或者信号机处于关闭状态SigStatus=0，三者只要有一个满足，则就到InvalidComm位置，认为是无效命令，将计时器clock_TU清零，回到初始状态。
4.6    各模块间的消息处理流程、建模以及模拟仿真
4.6.1    消息处理流程分析
在各进路控制流程中，联锁需要和ZC、ATS、还有各模块之间等进行大量的信息交换，为保证信息交换的安全有效，因此需要在联锁的每次信息传递过程中做一些处理来保证信息有效传达。这里我们把信息处理流程作为一个独立的模块单独提出来，用来验证消息传递的正确性。当接收方收到消息后会发送一个反馈消息，如果超时没有收到这个反馈消息后，就认为通信出现故障。各模块的消息处理流程如图4.34。 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(19):http://www.751com.cn/shuxue/lunwen_767.html