铁路信号联锁逻辑形式化建模研究

陈 良

（中铁十九局集团电务工程有限公司，北京 100076）

0 引言

在列车的通信系统中，计算机联锁系统是重要的设备之一。而随着计算机联锁系统的不断优化迭代，其内部系统构造越来越精密、复杂。该系统不仅需要对逻辑的运算，进而控制信号机、道岔、站台门、联锁进路等装置的联动控制，还需要与外部系统的信号进行即时对接。在逻辑的运算时还涉及了非常庞大的内部状态空间，而在与外部系统对接时通常会有大量的不确定性因素叠加，所以这类系统是一种非常精密、严苛的系统。有关资料显示，形式化的研究对提高软件质量有着重大贡献，其优势由此显现。

1 铁路信号与铁路计算机信号系统的内容

从铁路交通角度来看，铁路的信号是一个极其重要的领域。依据传统方式可以对铁路的信号进行归类划分，当列车的自动控制系统应用在城市轨道交通时，这种就是一个子域。近年来，在另外的3 种子系统中也不断地开始应用计算机技术。而利用计算机技术去解决铁路信号领域中出现的问题，也是一种非常方便、实用的技术手段。在铁路的计算机系统中，包含很多不同种类的子系统，而在一个调度区域内，区间闭塞与车站联锁都是与列车运行相关的部分。而在计算机信号系统中，色灯信号机、电动转辙机、轨道电路就是3 个室外的基础设备，而对行车进行指挥则是基础设备必备条件。整个的列车运行、停车都需要计算机的信号系统支持。系统控制层不仅是区间闭塞系统与车站联锁系统的核心，并且还是系统逻辑计算性能的实现者。

2 铁路信号联锁逻辑形式化建模研究

2.1 形式化研究

2.1.1 通信的程序进程

本质上通信程序的进程是根据进程代数而演变的形式化方法，其主要使用于并发系统与分布式系统中。其基本原理是：对系统中的进程交互，实现了描述与分析，并且形成了实体的数学框架。在进程内部中，可以实现信号的互相交互进而产生关联性影响，并且这种方法经得起严密的数学逻辑考察。其主要运作内容是对进程中出现的事件进行细小的描述，并且进程之间可以进行运算，然后与运算结果进行重合，进而实现对复杂问题进行详细的描述。而运算里包含并发进程、选择进程、混合进程等。而进程的事件，如果发现相同事件可以交互，则把这种事件叫做通信事件。

2.1.2 B 方法的应用

B 方法是种依据状态的形式化方法，可以通过数理推算和逻辑运算，从而建构起数学理论的框架。其优点在于可以建造软件系统的特征与状态，证明该框架的语法正确性，还能让模型得到进一步的精细化，从而让抽象模型变得更加具体。抽象机是B方法中的基本构成单位，抽象机的组成部分为变量、不变式、初始化、抽象机名等。

2.1.3 B 方法与通信程序进程的有机结合

这两种方法的结合，主要是考虑通信程序的进程是以“事件驱动”模式进行验证的，只适合对单一空间的软件系统进行描述。而B 方法虽然不适合单一空间的软件系统描述，但正因为如此，才可以刚好弥补通信程序进程这一缺点。对这两种方法进行互补式使用就一定可以满足对复杂或单一空间的描述与分析。而它们连接的关键点在于，在开始两种方法的操作之间建立起一个能够实现一对一的关系。只要能做到这两种方法的同步，就可以做到对复杂、单一空间的监控与管制。

2.1.4 有色PETRI 网的方法

有色PETRI 网（对离散并行系统的数学表示）分为分为层次有色PETRI 网与非层次有色PETRI 网两种，前者即HCPN（基于分层有色PETRI），其中包括了很多的非层次的有色PETRI 网。而层次的PETRI 网是对多个的HCPN 模型进行复合，使其的承载量变得更大。由此就能为非常复杂的空间提供分析与验证了，而这种方法的使用和高级程序开发语言所使用的层次。在HCPN 中，变迁方式为替代变迁与源变迁。而非层次的有色PETRI 网是理论基础非常完善的形式化语言，但同时也有图形结构，是建模工具的一种。而有色PETRI 网还可以为许多的实践应用做建模起到非常重要的作用。在目前看来，对于有色PETRI 网的定义还存在一定的争议。

2.1.5 TIMED SYNCCHARTS 建模方法

一般情况下，这种建模方式先要定义一个六元组，而SYNCCHARTS 是根据STATECHARTS 形式化的建模方式。但它并不具备时钟约束，而且它的层次结构太过简单，所以必须要定义好它的时间约束，并且还要做相关的宏布分析等计算工作。

2.2 铁路信号联锁逻辑形式化建模

2.2.1 信号联锁的属性特征

在铁路中，车站信号联锁系统的主要作用是对行车安全进行管控，该系统的功能主要有进路空闲检测技术、联锁技术、故障—安全技术等。而在车站的实际作业技术运用中，被分为调车作业与列车作业。但无论是哪一种作业，都必须遵从从某一指定地点到另外一个指定地点运行。而以列车为中心点，出发站与开入站和列车中心点的距离叫做进路，所以在进路中，必须先要保证列车调车作业的安全性。而想要达到这一效果，应当先要在进路的入口位置放置防护信号机的设备。而按一般情况来看，铁路的中线路较多，线路的两端都连接着道岔，可以按照道岔的位置设置对应的进路。如果要检测列车的进路是否畅通，可以通过信号机的信号收发来查看。如果信号机显示指示列车、车列进入轨道，但道岔位置却在另外一边，就会产生交通事故。所以，为了保证行车安全，必须要保证充分使用信号机。最后，需要建立进路，将进路中的道岔转变为进路的指定位置，随后开设防护信号机。如果道岔位置失误，信号机的开放就会出现“失败”的字样。另外，在信号机的开设过程中，位于进路中的道岔不可以被随意变换位置。这就是道岔的联锁与信号机的关联作用，而信号机对进路与进路、道岔与进路等主体都存在关联方关系。

2.2.2 开始铁路信号联锁的建模

铁路信号系统联锁复杂性，因为其本质上逻辑严密、复杂性强、车站作业种类等多种因素相关。如果规模比较小，作业形式单一，再加上车站周边的地理结构简单，那与之对应的信号联锁系统就比较简单。但是，对像上海、北京这样的大城市来说，其铁路的信号联锁逻辑系统就非常复杂。而CBTC（Communication Based Train Control，基于通信的列车控制）的计算机联锁系统面向对象是城市轨道交通，它可以通过计算机、信号机、通信等结合在一起，从而更好地实现对联锁进路、信号机、站台门等设备进行动态的监控。让通信接口与区域型的控制中心、列车自动监控系统、线路电子单元等外部系统进行即时信息传输，从而一同完成列车运行的控制，保障好列车的出行安全。而CBTC 联锁系统的逻辑运算有非常复杂的空间，可以用B 方法进行建模，其具体的步骤是联锁进路控制、站场信号的平面图等。其系统与外部系统连接因为存在非常大的不确定性，因此与外部系统连接的部分可以采用通信进程来进行建模。而关于B 方法对CBTC 联锁逻辑状态的运算，先要计算其核心，就是联锁进路抽象机。由于其独有的复杂性，所以可以采取分步精化。就是说，先建造一个初始状态的联锁进路的控制抽象机，然后再一点点添加相关的操作与状态，让它变得更加完善。在完成各类的抽象机计算之后，开始用通信进程来建构与外部交互的过程进行计算。最后开始对CBTC 进行分步精化。

第一步，添设紧急停车、站台门等设备的状态数据，并且补充这些状态的数据，需要满足其不变式的关系。按照进路原则检查，将这些数据填充到进路操作部分。

第二步，与进路的锁闭过程结合，添加已开放区域、进路的锁闭状态的数据，并给不变式做填充。

第三步，与进路开放的过程结合，添设信号机的数据，并补充相关的不等式。

第四步，进路的关闭，这里添加封闭信号机等的数据，继续补充与之对应的不等式关系。

最后一步就是与进路的解锁过程相结合，在开始解锁进路时，添加“三点检查”等比较安全的解锁逻辑规则。

对CBTC 的形态化验证，就是用原有的系统软件检测其是否可以满足它的约束条件。而当前比较多见的验证方法为模型检验。但是计算机的联锁或可以采用层次有色PETRI 网来对复杂的空间进行描述，而HCPN 模型就可以展开分层式的描述。因为层次有色PETRI 网具备完善的形式语言和图形结构，所以特别适合对计算机的联锁进行描述，首先要根据其理论结构基础，对于各个层面上的联锁实体组建相对应的HCPN 模型，组合后就可以形成一个完整的模型，而这时建立的模型才是联锁系统的HCPN 模型。而在铁路信号系统中，不仅有联锁关系，还有其他的运行规律。其建模的主要目的在于以更精确地形式化使联锁设备变得更容易控制，所以，同样也可以把车站信号的联锁分层、分类，这样才能更好地对联锁系统进行“分解”。

3 结束语

在铁路号联锁逻辑中，对于形式化的建模研究，可以采取多种多样的方式进行建模。本文简单探讨了B 方法与通信进程的结合使用，介绍了CBTC 计算机信号系统的建模。随着城市交通轨道的大力发展，计算机式的联锁系统模式必将引领新的交通系统技术，而传统的电联式的联锁必将逐步“退役”。只有交通系统大量迭代新颖的技术、高端的技术才能为人们出行带来实惠，才能提供更好的交通质量、速度、安全服务。另外，铁路交通系统不仅会因为更换高新技术而带来更加稳定、更令人满意的体验，还可以更好地占领市场，为地铁、铁路的运营带来实实在在的利润。