分散控制计算机联锁系统建模的研究

黄 菊 西南交通大学信息科学与技术学院

1 引言

联锁控制系统是保证列车安全运行的关键技术。目前普遍采用的联锁系统属于集中控制联锁系统，逻辑运算由联锁主机完成，联锁主机故障将导致整个系统无法运行。如果站场改造，逻辑联锁关系发生改变必须停止整个运行的联锁系统来修改联锁表，影响运输效率。为了满足越来越复杂的站场结构以及要提高铁路运输效率的要求，近年来提出了具有更高可靠性的分散控制计算机联锁系统[5,6,7]。该系统取消了联锁主机，基于全电子技术以信号机、道岔和轨道电路区段为基本单位分别设置对应的电子模块单元，通过这些电子模块相互协作完成进路联锁逻辑运算控制。目前国内外仍然处于理论研究阶段，没有实际应用。

该联锁系统进路控制功能通过模块间频繁的通信来实现，有较强的时间约束，属于复杂实时系统。该系统建模采用基于时间自动理论的模型验证工具UPPAAL，通过仿真时序图分析系统信息交换情况，验证系统功能特性、安全性和时间特性。

2 分散控制计算机联锁系统的建模与验证

2.1 分散控制计算机联锁系统

分散控制计算机联锁系统也可叫分布式计算机联锁系统[6,7]，是相对于目前集中控制联锁系统而提出的一种全新概念。它由操作表示层、通信网络层和逻辑控制层组成。将传统集中联锁逻辑功能分散到各个电子模块，通过电子模块相互协作完成进路的建立和解锁（如图1 所示）。

操作表示层[6]是人机交互的界面。负责实时显示站场设备状态、操作状态和各类电子模块的状态；完成调度命令输入，形成操作指令并发送到逻辑控制层；此外还包含文字和语音的操作提示。维修机相当于微机监测系统，完成系统的监视功能，实时记录设备运行情况，包括来自上位机的操作信息、逻辑控制层的数据和故障信息等。

图1 分散控制计算机联锁系统结构图

通信网络层完成操作层与逻辑控制层之间的通信，以及逻辑控制层电子模块与电子模块之间的通信。

逻辑控制层包括信号机电子模块、道岔电子模块和轨道电路电子模块，每个模块都是全电子模块，相当于一台微型计算机，完成联锁逻辑运算和现场信号设备的驱动采集功能。

被控设备层指现场设备，包括信号机、道岔和轨道区段。它们在物理上完成联锁逻辑命令，实现车站联锁功能。以站场图（见图2）举例分析分散控制计算机联锁系统进路控制过程。

图2 站场图

调度员通过终端操作机先后按压XLA 信号按钮和S3LA信号按钮。操作层对进路进行合法性检查，通过静态联锁表查找到始端信号机ID 号，将进路命令发送到始端信号机电子模块。

（1）选排阶段

①X 接收进路命令后，判断本信号机是否空闲，是否被征用或者故障，满足条件，根据进路号查找联锁表中参与进路的电子模块信息，将进路选排命令发送给参与进路的电子模块，等待模块回复信息，在一定时间内根据回复的信息进行联锁逻辑判断。

②C1 和C5 接收进路选排命令，判断道岔是否锁闭，是否参与其它进路控制，满足条件将进路要求的道岔位置与采集道岔状态比较。道岔在规定位置，回复始端信号机道岔满足条件；如果不在规定位置，生成道岔控制命令，在规定时间内道岔转换到规定位置将信息返回始端信号机，否则将失败信息返回始端信号机。

③D1、D5 和S3 作为敌对信号接收到进路选排命令，检查是否已被征用或者故障，回复始端信号机敌对信号情况。

④ⅠAG、1DG、5DG 和3G 轨道区段电子模块接收进路选排命令，检查区段是否参与其它进路控制、是否锁闭、是否空闲，回复始端信号机轨道区段情况。

（2）进路锁闭

①X 发送锁闭命令，等待锁闭信息回复。

②D1、D5 和S3 接收命令，再次检查锁闭条件，设置进程标志，返回锁闭信息。

③C1 和C5 接收命令，再次检查道岔锁闭条件，设置锁闭标志，返回锁闭信息。

④ⅠAG、1DG、5DG 和3G 接收命令，再次检查区段锁闭条件，设置锁闭标志，返回锁闭信息。

⑤X 在规定时间内根据电子模块返回的锁闭信息后，判断进路是否锁闭，设置进程标志。

（3）信号开放

①X 检查信号机灯丝是否故障，发送信号开放检查命令，等待信号开放条件回复。

②ⅠAG、D1、C1、1DG、D5、C5、5DG、S3 和3G 再次检查信号开放的条件，回复X 检查结果，X 根据检查结果，判断开放条件是否成立，生成信号开放的驱动命令。

（4）信号开放保持

①X 检查灯丝的完好性。

②X 与ⅠAG、D1、C1、1DG、D5、C5、5DG、S3 和3G 保持通信，检查信号开放的条件，并获得列车占用信息。

③当列车进入ⅠAG 时，区段将信息发送给X，X 立即关闭信号。

④如果有列车越过了ⅠAG，直接进入1DG 或者5DG 或者3G，返回故障，关闭信号。

（5）进路解锁

①X 正常关闭后，发送解锁命令，等待解锁信息回复。

②C1 接收解锁命令，检查1DG 是否已经解锁，接收到1DG 的解锁信息，那么道岔可以解锁，设置锁闭标志，消亡进路对本模块的占用，返回解锁信息；C5 同理。

③D1、D5 和S3 接收解锁命令，设置进程标志，消亡进路对本模块的占用，返回解锁信息。

④ⅠAG、1DG、5DG 和3G 在接收解锁命令，相互通信，得到列车占用出清情况，进行解锁条件的判断。ⅠAG 满足"两点"检查，1DG、5DG 和3G 满足"三点"检查，设置锁闭标志设置，消亡进路对本模块的占用，返回解锁信息。

⑤X 在接收所有模块的解锁信息后，解锁该进路，消亡进路对本信号机的占用。

通过以上分析，可见进路控制过程的着力点在始端信号机电子模块和参与该进路的其它电子模块，如果一个模块故障，只影响与该模块有关的进路，并不影响站内其它进路，所以在一定程度上分散了故障点。

2.2 时间自动机模型

采用基于时间自动机理论[1,2]的UPPAAL[3,4,8]对系统进行建模，该理论已经很成熟，不再详述。以下以一条列车接车进路的进路选排过程为例说明信号机、道岔、区段电子模块之间的协作关系。对操作层、始端信号机、轨道区段、敌对信号和道岔电子模块分别建立时间自动机模型（图3 为操作层建立时间自动机模型，始端信号机、轨道区段、敌对信号和道岔电子模块与图3 类似）。

图3 操作层时间自动机模型

2.3 模型分析验证

模型建立后，在模拟器中随机运行可得到仿真时序图。通过仿真时序图可观察模块之间信息的交互情况，如图4 所示。

操作层与始端信号机在2 个时间单位内通过Route_Com和Com_Reply 通信；始端信号机对进路命令进行处理后，在1个时间单位内向道岔、轨道区段和对信号电子模块发送CheckCom 选路检查命令；道岔、轨道区段和对信号电子模块不管满足选排条件与否都必须在2 个时间单位内完成检查并回复始端信号机检查情况，分别通过SuccT、SuccSw、SuccCs 或者FailT、FailSw、FailCs 进行信息交互。如果道岔位置不在规定位置，道岔电子模块生成道岔驱动命令，通过SetTime启动内部时钟，如果在13 个时间单位内完成道岔的转换，通过Reset 复位时钟，反之道岔转换失败，进行故障处理，发出TimeOut 时间溢出信息。同时在验证器中使用属性验证语法可以对选排阶段的功能性质进行验证。如A[] not deadlock 通过验证，表明模型不会出现死琐；A<>Switch.ChangeSwitch imply SwPosNow==0 通过验证，表明只有道岔位置不符合进路要求位置时才会转动道岔；A<>FirstSignal.count! =3 imply route==1 未通过验证，表明有电子模块不满足选排条件，进路选排失败。其它性质也可以通过逻辑公式进行验证，在此不详述。

图4 进路选排的仿真时序图

3 总结

本文介绍了分散控制计算机联锁系统的结构及功能特点，用UPPAAL 对分散控制计算机联锁系统进行建模。通过仿真时序图分析了模块之间的通信过程和状态。进路选排模型展现了信号机、道岔和轨道区段电子模块在进路控制中的协作关系。虽然验证了分散控制计算机联锁系统的部分功能性质，但后期还可以对系统进一步深化，考虑更全面的进路控制过程、更多的故障状态和更多的电子模块使模型更精准，才能为分散控制计算机联锁软件设计提供参考。

[1]R.Alur,D.L.Dill,A theory of timed automata.Journal of Theoretical Computer Science, 126(2):183-235,1994.

[2]王静.基于时间自动机的模型验证理论及应用研究[D].郑州大学.2005.

[3]G.Behrmann,A.David,and K.Larsen.A tutorial on Uppaal.In Formal Methods for the Design of Real-Time Systems,Springer Verlag,2004,Lecture Notes in Computer Science,Vol.(3185):pages 200-236.

[4]http://www.uppaal.com/.

[5]Hei X,Takahashi S,Hideo N.Toward developing a Decentralized Railway Signalling System Using Petri Nets [C].Robotics, Automation and Mechatronics, 2008 IEEE Conference on. IEEE, 2008: Pages851-855.

[6]于飞.分散控制计算机联锁系统网络通信研究[D].西南交通大学.2012.

[7]陈晓伟.新型分布式计算机联锁系统的研究与设计[D].兰州交通大学,2009.

[8]王观宁.基于UPPAAL 的联锁进路控制流程建模与验证[D].北京交通大学.2009.