图4.34  各模块间的消息处理流程图
4.6.2    消息处理模型
 
图4.35  联锁消息处理的时间自动机模型
联锁的进路控制流程也是和其他模块进行消息交流的过程。当联锁与其他模块的消息传递没有在规定时间内收到回复，则要进行相应的故障处理。
通常的超时处理做法是，发送端在发送消息a的同时会启动计时器。接收方收到消息a后，向发送方发送一反馈消息b。如果发送方在规定的时间内没有收到对方的反馈消息b，则认为出现通信故障。图4.35是联锁消息处理的时间自动机模型。
表4.7  消息处理模型主要位置、通道说明表
位置集合    通道集合
主要位置    说明    通道    说明
Idle    初始位置    RFC    请求建立链接
waitACK    等待ACK    ACK    建立链接应答
StartComu    开始正常通信    App_data    发送应用数据
settimer    设置定时器    SetTimer    时钟启动命令
WaitData    等待接收数据    timeout    超时报警
AppProc    应用处理阶段    Reset    时钟复位
Send    发送数据    NO_DATA    没有应用数据回复
noReplydata    没有得到回复消息    DATA_Reply    有应用数据恢复
check    检查是否超过最大周期    error    超时错误处理
Resend    应用数据重发        
Error_proc    错误处理状态        
当联锁发出RFC请求建链，接收方返回ACK后表示建立通信的连接。随后联锁发送应用数据并同时启动计时器。这时对于消息接收方的处理有两种情况：一种是在规定的时间内发送反馈消息，一种是超时没有回应，所以我建立了两个子模块来模拟接收方的消息处理。如图4.36所示。
          
图4.36  消息回复和未回复的两种时间自动机模型
右图表示在一个收到反馈消息，通过DATA_Reply传递给联锁：左图表示没有收到反馈消息，通过通道NO_DATA传递给联锁。
在规定时间内收到消息后，联锁还要通过变量haveAffirm判断这些消息中有没有还未确认应答的消息，就是发送方可以发送新数据还是需要重新发送一遍刚才的消息，如果有则重发消息（Resendmessg（））；如果没有则发送新的消息（newMessg（））。如果超时没有收到对方的反馈消息，变量MAX_Time用来计算没有收到记的次数，连续5次没有收到数据，则表示通信故障，进入故障处理状态，不能办理进路。消息是否超时，主要靠时钟模块来控制。其时间自动机模型如图4.37所示。
 
图4.37  消息处理的定时器模块
这里我们需要一个启动模块来模拟当联锁发出请求RFC后，接收方收到后返回ACK，这里我们做了一个简单的接收模块，如图4.38所示。
 
图4.38  消息处理的接收方模块
这里消息处理超时后进入故障状态，为了不让进入故障状态后又被重新启动，这里添加了一个故障修理模块，即进入故障后就认为其在修理中，令Repair置1，在启动时先要判断Repair是否为0，如果为1则说明在修理，则无法启动。模块如图4.39所示。
 
图4.39  消息处理的故障修理模块 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(20):http://www.751com.cn/shuxue/lunwen_767.html