进入应用数据的正常收发阶段后，联锁在发送应用数据首先向接收方模块发送RFC，接收方收到后回复ACK，同时向时钟Timer_DATA发送SetTimer启动时钟计时，如果超过规定的时间还没收到反馈消息，模块NoReply_Data会发出NO_DATA，超时后发出超时报警timeout1，并计数器MAX_Time加1，满5次后进入故障修理状态，并且令Repair置1，不能再被启动，直到人为修正。变量MAX_Time为周期计数器，当记满五次后则认为进入故障处理状态。变量NoReply等于1或0来表示有无应答。
4.6.3    消息处理模拟仿真
 
图4.40  消息正常收发的消息序列
当联锁发出RFC！命令，来到waitACK位置，等待接收方回复ACK命令，接收方模块回复ACK命令，来到启动位置StartComu，发送App_data！命令，并将计时器Cycle_T置0，这时会启动reply_data模块，并来到settimer位置，发出SetTimer！命令，启动timer_data模块，并来到WaitData位置，由于前面启动了reply_data模块，会发送一个DATA_Reply命令，并判定NoReply是否等于0，判定符合后将计时器MAX_Time清零，来到AppProc位置，然后通过变量haveAffirm来判定消息是否有还未确认过，当还没有确认过则重新发送数据，当已经确认过了则发送新的数据，发送后来到Send位置，然后到resttime位置，最后发送Reset！命令，重置timer_data模块，回到StartComu位置。
 
图4.41  通信故障的消息序列
图4.4.1为消息处理时通信出现故障的消息序列。当联锁发出RFC！命令，来到waitACK位置，等待接收方回复ACK命令，接收方模块回复ACK命令，来到启动位置StartComu，发送App_data！命令，并将计时器Cycle_T置0，这时会启动noreply_data模块，并来到settimer位置，发出SetTimer！命令，启动timer_data模块，并来到WaitData位置，前面启动的noreply_data模块会发出一个NO_DATA命令，然后判定Cycle_T>=5秒，并且NoReply=1，判定符合后来到noReplydata位置，timer_data模块会将计时器t置0并启动，5秒后没有收到重置命令则会发送timeout命令，消息处理模块收到这个命令以后将MAX_Time计数器加1，来到check位置，然后判定计数器有没有超过5，没有超过则来到Resend位置，将计时器Cycle_T清零，发送App_data命令，并发送SetTimer命令，重新启动noreply_data模块、timer_data模块，并回到WaitData位置，当这样反复到第五次后，则在check位置向另一方向走，来到error_proc位置，发送error命令，启动repair模块，将Repair置1，并来到mid3位置，最后回到idle位置。
这里我在建模的过程中发现，repair模块中的Repair变量，一开始我使用小写repair，然后运行时出现报错，经过几次修改后发现，一定要将小写改成大写Repair，不能让变量名与模块名出现冲突。
5      结论
计算机联锁是信号系统的重要组成部分，对于保证行车安全起到了十分关键的作用。铁路的计算机联锁不仅复杂，而且由于其高速性，还增加了许多特殊的功能来保证其安全性、实时性等。
本论文的主要工作有以下几点：
首先是介绍了铁路的发展背景，以及铁路的发展现状，然后介绍了计算机联锁系统的一些概况和发展状况，还以及选题的目的及意义。
介绍了形式化方法的概况，对计算机联锁系统的故障安全原则也进行介绍，让大家了解了什么是故障导向安全，介绍了时间自动机理论，因为这里我们以UPPAAL为时间自动机理论的基础，所以然后着重介绍了下UPPAAL这个软件和它的结构和特征。
这里我们提出了安全苛求系统的开发要求，提出了联锁软件设计开发的框架模型。然后进行了需求分析，根据分析，对办理进路的每一个阶段进行形式化建模。 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(21):http://www.youerw.com/shuxue/lunwen_767.html