基于时间自动机的监测系统通信流程建模分析

高 昕

(国电南瑞科技股份有限公司，211800，南京∥工程师)

铁路信号设备是重要的铁路行车设备，加强对铁路信号设备运用状态监督和管理，有助于提高铁路信号设备的工作效率和稳定性，进而减少故障发生率。

通过建模能够模拟系统的运行，建模是分析、研究系统性能的有效手段。在建立系统模型时做必要的抽象和假设，对系统的主要功能和特性进行合理说明和设计，忽略与研究分析不相关的细节，将有助于突出研究的重点，完成系统重要特性的验证。

1 轨道电路微机监测系统中的通信协议介绍

轨道电路微机监测系统主要由采集终端、采集处理机及微机监测站机3部分组成。采集终端负责从轨道电路设备采集电压、电流、频率以及开关量并定时传送到采集处理机;采集处理机需要能够正确地读取采集终端发送的各种数据信息，包括开关量、模拟量、CAN(网络)设备状态及报警信息等，并对信息进行分类处理后发送到监测站机;监测站机用于接收采集处理机发送来的监测信息，对轨道电路的状态进行实时监测。

1.1 串口通信的数据帧类型

根据通信协议，采集处理机与微机监测站机之间需要用6种类型的数据帧交换(如表1所示)。其中的ACK(通信允许)帧及ZPW_DATA(周期性报文数据)帧是由监测站机发送，其它4种由采集处理机发送给微机监测子系统。

表1 串口数据帧类型

1.2 通信流程分析

按照上述通信格式及通信内容，微机监测站机与采集处理机的数据帧交换流程可简单概括如下:

(1)监测站机请求与采集处理机通信或通信复位时向采集处理机发送ASK帧;采集处理机接到ASK后，以ASK帧中包含的时间信息校正自己的程序时间，将发送帧序号置1，然后以ACK帧应答。

(2)监测站机接到ACK帧后，表示与采集处理机的连接成功，同时设定面向该连接的定时器。如果2 min没有接收到采集处理机发送来的任何数据，则重新发送ASK帧。

(3)监测站机10 min向采集处理机发送一次TIME帧，用于校正子系统中采集处理机软件的程序时间。

(4)采集处理机每分钟向微机监测站机发送ZPW_DATA数据帧，该数据帧中包括全站的所有数据信息。

(5)微机监测站机接收数据的过程中，若发现了发送序号的不连续跳变，则认为出现了数据丢失，则将缺失的帧序号包含于Resend帧中发向子系统，采集处理机根据该序号重新发送该帧。

(6)当出现报警信息时，采集处理机在发向微机监测站机的ZPW_DATA帧中对某一标志位置1，表示报警信息。微机监测站机接到该报警信息后，向采集处理机发回ZPW_ACK帧。如果采集处理机发送了报警信息帧后没有收到微机监测站机发来的ZPW_ACK帧回应，则对该报警信息间隔2 s定时重复发送3次。

ZPW－2000A子系统对微机监测站机的通信流程时序如图1所示。

图1 采集处理机与监测站机通信时序图

2 时间自动机及实时系统验证软件UPPAAL

自动机理论(Automata Theory)是在开关网络理论和数理逻辑中图灵机理论的基础上形成和发展起来的。现在己经成为研究离散数字系统的功能、结构以及两者之间关系的有效数学工具，成为理论计算机科学的重要组成部分。

时间自动机是在传统有限状态自动机基础上为迁移添加时钟约束，为状态添加不变式约束而得到的。列举一个可调亮度节能灯的例子来说明时间自动机的模型。假设一个灯泡具有关闭(off)、低亮度(low)和明亮(bright)3个状态。3个状态之间的转换方式是:如果用户在关闭状态下按下开关，则灯泡进入低亮度状态，再按开关则灯泡关闭;但若用户迅速按下开关两次，则灯泡变成明亮状态。其时间自动机的模型如图2所示。

图2 节能灯的时间自动机模型

图2中a)表示节能灯的模型，b)表示用户按下开关的操作。用户可以随机地按下几次或不按开关。开关按下后，使用通道Press(按)来传递同步消息。时钟变量y用来监测用户按下开关的间隔频率为快(y＜5)或慢(y≥5)。

UPPAAL是由丹麦的 Aalborg大学和瑞典的Uppsala大学于1995年联合开发的一个基于时间自动机的验证工具，已经在通信协议、多媒体等众多领域成功应用。它特别适合实时系统的安全性和有界活性的自动验证，不仅可以有效地发现系统设计中出现的错误，而且可以清楚地显示导致出现错误的判定路径。

UPPAAL的用户界面包括系统编辑器(system editor)、模拟器(simulator)和验证器(verifier)3个主要部分。系统编辑器用于创建和编辑要分析的系统，一个系统被描述为一系列过程模板、一些全局声明、过程分配和一个系统定义。验证器通过快速搜索系统的状态空间来检查时钟约束和活性，它还为系统要求的规范和文件提供了一个需求规范编辑器。

3 监测系统通信流程的建模

在使用UPPAAL建模时至少需要建立2个模板分别用来代表监测站机的通信模型和采集处理机的通信模型。另外，随机产生的数据丢帧的情况也使用一个独立的模板为系统提供随即命令的发送。

在通信系统模型中，一共涉及9个通道变量，可分为 3 组:① chan ASK，ACK，Resend，TIME，ZPW_ACK，ZPW_DATA;② chan Alarm，DataLost;③broadcast chan AlarmLost。

其中，第一组通道用来模拟通信系统中传递的数据帧，比如ASK表示微机监测站机系统向采集处理机发送了ASK帧。第二组和第三组用来模拟报警、数据丢失及报警信息丢失的情况，属于辅助通道。另外第三组还为广播通道，可以同时使2个模板同时接收通道命令。

使用UPPAAL软件对系统进行建模时，需要对系统的各个状态及功能使用一个位置(Location)来表示。在UPPAAL软件中建立的微机监测站机通信功能的模型如图3所示，该图为UPPAAL软件界面截图。

图3 监测站机通信的时间自动机模型

此通信模型中有bool变量和int 2个时钟变量，另外还有一个全局变量FrameIndex，用于在2个模型之间传递帧序号。各个变量所表示意义见表2。

表2 监测站机模型中的变量名称及意义

子系统采集处理机模型多数情况下都是接受监测站机发送来的指令，然后按照要求应答。

为采集处理机通信功能建立的时间自动机模型如图4所示，该图为UPPAAL软件界面截图。

在对子系统采集处理机进行建模分析时，模型中涉及到了3个clock变量、2个int变量及一个bool变量，各个变量所代表的意义见表3。

4 通信模型功能的验证

使用UPPAAL软件中的系统验证功能可以根据输入的验证语句进行系统功能的验证。在UPPAAL软件中，对性质的验证使用绿灯表示性质满足，红灯表示性质不满足。同时在验证窗口的底部，通过中文显示了某验证的性质是否满足。以验证死锁为例，性质A［］not deadlock表示系统一定无死锁，其完全相反的性质为A［］deadlock，表示系统一定存在死锁。

图4 采集处理机通信的时间自动机模型

表3 采集处理机模型中的变量名称及其涵义

在对系统进行建模后，自建了一些简单的验证语句，基本上能够涵盖了系统的通信功能的验证。对系统功能验证的语句如下。

(1)A［］not deadlock 含义:系统模型需要满足的第一条语句，表示系统在任意状态位置时不能出现死锁的情况。若此条件不满足，则其它的所有验证都是没有意义的。

(2)A［］M.GetASK imply S.WaitACK 含义:采集处理机获取到ASK帧时，暗示监测站机一定在等待ACK帧。

(3)A［］S.SendTIME imply(S.Time600≥600 and S.S_Commok==true) 含义:监测站机系统发送了时间校正TIME帧，一定暗示了通信正常并且已经间隔了10 min。

(4)A ＜ ＞ (S.Time600 ＞ =600 and S.S_Commok==true)imply S.SendTIME 含义:监测站机通信正常状态每10 min将会发送一次时间校正TIME帧。

(5)S.Time120＞120－ － ＞not S.SendTIME含义:监测站机系统120 s没有收到数据，一定导致停止发送TIME帧。

(6)A ＜ ＞ A.LostData imply S.LocalIndex+1!=FrameIndex 含义:数据帧的丢失将造成监测站机保存帧序号与发送帧序号的跳变。

(7)A.LostData and S.S_Commok==true－ －＞M.ResendData 含义:监测站机通信正常且出现数据丢失时，将导致采集处理机重发数据。

(8)A［］S.GetAlarm imply not A.LostAlarm含义:监测站机接收到报警信息，暗示一定没有错误或报警丢失。

(9)A.LostAlarm－ － ＞M.ResendALARM 含义:报警信息丢失将导致采集处理机重新发送报警信息。

(10)M.ResendALARM and M.n＞3－ － ＞not M.ALARM 含义:当报警信息已经重发3次后，将导致不再重发该报警。

5 结语

本文在介绍和分析轨道电路微机监测系统中采集处理机与监测站机间的通信协议的基础上，使用实时系统建模及分析软件UPPAAL分别建立了采集处理机与微机监测站机之间通信过程的时间自动机模型，将抽象的通信协议形象化。自建的10条的验证语句，基本上能够涵盖了全部的通信功能。这些验证语句成功通过验证，标志着模型在功能完整性、正确性及运行无死锁等方面均达到了协议的要求。

使用UPPAAL软件提供的验证功能确保模型功能的正常实现，使模型能够为轨道电路微机监测系统软件开发的思路进行指导，规范软件的模块化设计，缩短软件的开发周期，使编制出的软件尽量减少功能缺陷，满足功能的需求。

［1］曾欣.浅谈微机监测系统在信号设备中的应用［J］.铁道工程企业管理，2007(2):45.

［2］Aalborg.UPPsala.UPPAAL Help［EB/OL］.(2009 － 10 － 16)［2013 －05 －25］.http://www.uppaal.com.

［3］周清雷.姬莉霞.基于UPPAAL的实时系统模型验证［J］.计算机应用，2004，9(9):129.