图4.3  ATS的时间自动机模型
图4.3为ATS自动列车监控系统的时间自动机模型。ATS子系统主要是给联锁下达进路控制命令，联锁收到这些命令后，开始启动进路选排或者延时解锁等等的模块，经过一定的逻辑处理，进而控制进路、道岔、信号机等站场元件。相关模块收到命令后要将站场各元件的实时状态传回给ATS。由于这里只研究进路处理的各个阶段，所以ATS只需要给出办理进路的命令，联锁在收到命令后给出应答即可。
Route_App！命令为启动进路选排的命令，当判定进路状态routestatus=0并且ats_T大于等于60秒，当满足时则发送Route_App！命令，并将需要办理的进路ID赋值给变量RouteID，当收到返回来的App_Reply命令后回到初始状态，并将计时器ats_T清零。
TimeUnlockApp！命令为启动延时解锁模块的命令，当判定进路状态routestatus=4，并且人工解锁ManualUnlock=1时，发送TimeUnlockApp！命令，并将需要办理的进路ID赋值给变量RouteID，当收到返回来的UnlockReply命令后回到初始状态，并将计时器ats_T清零。
 
图4.4  ZC的时间自动机模型
图4.4为ZC的时间自动机模型。联锁在解锁阶段的空闲检测需要ZC来告诉区段占用情况。通过列车的位置汇报来转换成区段的占用空闲信息，联锁根据这些信息对进路进行解锁。FirstFree_App命令为启动ZC模块右侧部分的命令，当收到这个命令后到Wait位置，等待检测监测轨占用情况，当有车占用FirstSecStatus=1，没有车占用FirstSecStatus=0，并发送ZCInfor命令。RouteFreeApp命令为启动ZC模块左侧部分的命令，当收到这个命令后等待检测区段占用情况，通过变量Occupied来表示，如果有车占用Occupied=1，没有车占用则Occupied=0，并发送ZC_RouteOcc命令。
 
图4.5  道岔控制的时间自动机模型
图4.5为道岔控制模块。由于每次办理完进路后按照联锁表，一定会要求相应的道岔在一个规定的位置，然而道岔控制功能将直接影响列车移动的安全，所以它将拒绝执行不符合安全条件的命令，在办理进路后会转换到规定的位置。
道岔启动过后应该是能够转换到规定的位置。当因为故障不能动作或者说被大石头卡住不能移动到规定位置时，如果在规定的时间内不能转换到规定的位置时，就要进入故障处理，并且发出Disaccord，表示道岔与规定位置不一致，需要重新进行进路选排。
表4.2  道岔控制模型主要位置、通道说明表
位置集合    通道集合
主要位置    说明    通道    说明
Idle    初始位置    SwitchCommd    道岔动作命令
SwitchChange    道岔转动    SetTimer_S    启动时钟
SwitchFail    转动失败    timeout1    超时警告
Error    故障处理    reset_S    时钟复位
ChangeOver    转动结束    Accord    道岔在期望位置
replyCom    回复道岔执行结果    Disaccord    道岔不在期望位置
用时钟switch_clock对这些位置进行时间约束。同时设置时钟Timer_Swic控制道岔转动时间，如果超时间仍没转到规定的位置，就会认为该道岔故障，进入故障处理。可以对时钟进行开启和复位操作。t1是该时钟模型内部的一个时钟，为超时的时间，如果设置成5秒则超过5秒就认为进入故障处理，当道岔开始动作会同步发出SetTime_S！命令，来启动Timer_Swic，启动后时钟处于check状态时，如果超时则发出timeout1警报，如果道岔动作到了规定位置后，会发送一个reset_S命令，让计时器归零，复位到初始状态。变量Failrelease用来判断道岔转动是否故障，如果故障则Failrelease=0，如果没有故障，道岔转到了规定位置，Failrelease=1。变量Posnow=1表示道岔开始动作。 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(12):http://www.youerw.com/shuxue/lunwen_767.html