基于CPN的联锁系统选岔网络建模及验证

陶 玲，宋 军

基于CPN的联锁系统选岔网络建模及验证

陶 玲，宋 军

在详细分析联锁系统选岔电路的前提下，抽象出选岔网络的联锁逻辑条件，并采用有色Petri网（Colored Petri Net，CPN）为其建立形式化验证模型，同时采用CPN TOOLS对所建立的模型进行仿真及状态空间分析，结果表明所建立的模型能够很好的描述选岔网络的工作状态。

选岔网络；CPN；形式化；CPN TOOLS

0 引言

铁路信号计算机联锁软件是铁路信号系统中非常重要的安全苛求软件，对保障行车安全至关重要，而针对联锁软件中联锁逻辑关系形式化验证方法的研究将有利于减少联锁软件开发过程中的不确定性，及时发现联锁软件的设计缺陷，降低联锁软件的开发成本。对于大中型站场，联锁逻辑关系非常复杂，如何建立正确的形式化验证模型，是联锁软件中联锁逻辑关系形式化验证方法研究的重点。选岔网络是保证联锁系统能够正确选出满足操作意图的进路的重要组成部分，为选岔网络建立正确的形式化验证模型是联锁软件形式化验证方法研究的重要内容之一。

1 有色Petri网系统

1.1 CPN

Petri网是一种基于数学和图形的描述分析工具，因其可使用图形和严格的数学定义来描述系统，所以对系统结构的描述较为容易，然而基本Petri网库所中的Token属于同一类型，个体之间没有区别，对于大型复杂系统的建模容易造成状态空间爆炸问题。有色Petri网（Colored Petri Net，CPN）是专门针对传统Petri网的局限性，结合传统Petri网的特征及高级编程语言的优势而发展起来的高级Petri网，主要由颜色集、声明、库所、变迁、弧、弧函数等组成，不仅具有直观的图形化表示，同时具有形式化的数学定义。在CPN中引入颜色集和分层的概念使得在使用CPN描述复杂系统结构时能够得到很大程度的简化，除此之外，CPN模型不仅可以直接描述异步并发系统的物理层次结构及系统中各种资源的初始分布状态，还可以展现出引发规则的作用下系统的动态行为机理。因此在众多的形式化建模方法和语言中，CPN建立的模型有利于动态仿真，适合具有同步、并发、资源共享的复杂系统。

1.2 CPN TOOLS

CPN TOOLS是丹麦Aarhus大学CPN研究组开发的专用于CPN模型设计、仿真和分析的工具。CPN TOOLS能提供模型化、可视化的模型开发环境及友好交互界面，可在模型建立过程中自动实现语法检查和代码生成，模型建立后，用户可使用仿真工具，动态执行所建模型，同时生成仿真报告，CPN TOOLS提供的状态空间分析功能，可对所建立的模型进行部分或全部的状态空间分析，生成的状态空间报告包括可达性、有界性、活性、公平性、家态性等网的性质。最新版本的cpn_tools 4.0.0在原有版本的基础上又增加了约束弧及重置弧的功能，使得用CPN TOOLS建立系统模型更加方便。

2 选岔网络

选岔网络用于自动选出进路上道岔的位置，在继电联锁中为了控制道岔的转向，对应每组道岔设置定位操纵继电器（DCJ）和反位操纵继电器（FCJ），分别控制道岔操纵到定位或反位，进路选出的含义是指与所选进路相关的所有的DCJ或FCJ都励磁（不包括道岔的转换），通过道岔的位置来确定进路开通的方向。选岔网络最重要的任务是必须能选出与操纵意图一致的进路。选岔网络包括以下防护条件：

（1）确保道岔选出定位后不能再选反位，或者选出反位后不能再选定位。

（2）只有在与所排进路所有相关道岔均处于解锁状态时才能选岔。

（3）在进路不能选出时可以通过总取消的方式取消选岔网络的工作状态。

（4）在车站值班员没有办理变通进路时，只能选出基本进路，而办理了变通进路后只能选出变通进路，不能选出基本进路。

以上防护条件只包含了对联锁逻辑关系做形式化验证建立CPN模型时所必须的防护条件，并不包含原继电联锁电路中由于自身的电路原因而必需的防护条件。

3 选岔网络CPN模型的建立

3.1 单动道岔定、反位的CPN模型

根据6502电气集中选岔电路可知双动道岔定位，单动道岔定、反位在道岔操纵继电器励磁及自闭电路中所检查的联锁条件是一致的，即必须有正负电源，道岔处于解锁状态，保证道岔处于正确的位置，保证在道岔不能锁闭时能随时取消，因此根据抽象出的联锁条件可为双动道岔定位，单动道岔定、反位建立相似的CPN模型，本文以单动道岔反位为例建立CPN模型如图1所示。

由于单动道岔反位控制的联锁条件较为简单，故建立的CPN模型也较为简单，模型中各颜色集均只包含一个元组，用CPN TOOLS提供的约束弧来满足相关的联锁条件，库所C、库所Lock、库所DC有Token时变迁src就不能发生，即道岔处于锁闭状态或道岔已操纵到定位或者进路处于取消状态时，均不能允许道岔操纵到反位。图1中各库所变迁的物理意义如表1所示。

图1 单动道岔反位控制的CPN模型图

表1 单动道岔反位控制各库所变迁的物理意义一览表

3.2 双动道岔反位控制的CPN模型

双动道岔反位可分为八字第一撇双动道岔反位及八字第二撇双动道岔反位，在继电联锁电路中由于存在电路迂回，同极性电流串电现象，故把八字第一撇双动道岔反位、八字第二撇双动道岔反位分别设计在不同线的电路上。但是在CPN模型中不存在上述由于电路自身原因而导致的问题，故可以用同一种CPN模型来建立2种道岔反位控制的模型。双动道岔反位控制CPN模型如图2所示。

图2 双动道岔反位控制的CPN模型图

图2中各库所变迁的物理意义如表2所示。

表2 双动道岔反位各库所变迁的物理意义一览表

3.3 变通进路的CPN模型

进路通常分为基本进路和变通进路，变通进路又分为八字变通进路及平行变通进路，如何使得车站值班员能够顺利的选出与其操纵意图一致的进路，是在设计选岔网路时必须考虑的重点。

3.3.1 八字变通进路的CPN模型

在继电联锁控制中通过增设变通按钮以及相应的电路来选择变通进路，增设变通按钮在选岔时的实质主要是为选变通进路时构成两段选路提供正负电源，借用6502的思想，在建立CPN模型时增设BKZ、BKF两个库所，为变通进路的两段选路提供正、负电源信号，以图3所示的站场为例，建立经5/7、17/19号道岔反位的变通进路的CPN模型如图4所示，由于不同站场中八字变通进路所需的防护原理是相同的，故由此所建立的模型可用在所有的八字变通进路中。

图3 八字变通进路示意图

模型中由于每一段选路均涉及2组道岔，因此每一个提供电源信号的库所均包含2个元组的托肯色，这2个元组虽然染上不同的颜色，但均表示为道岔操纵提供电源信号。与继电联锁相似，在CPN模型中用相应的约束弧作为同一组道岔定位操纵与反位操纵的互切条件，保证在变通进路选不出时，不会自动改选基本进路。图4所示的CPN模型中各库所变迁的物理意义如表3所示。

图4 八字变通进路的CPN模型图

表3 八字变通进路CPN模型各库所变迁的物理意义一览表

3.3.2 平行变通进路的CPN模型

在继电联锁控制电路中通过断线法来控制选出与值班员操纵意图一致的平行变通进路，在建立CPN模型时，不需要采用断线法，但可借鉴继电联锁电路中通过始端按钮与变通按钮、变通按钮与终端按钮相互配合选出变通进路的方法来建立模型。因此建立模型的方法与八字变通进路相似。

4 仿真及状态空间分析

采用cpn_tools 4.0.0对图1、图2、图4所建立的CPN模型进行仿真，发现所有的模型均能通过语法检查，在仿真的过程中既可对其进行单步仿真操作，也可对其进行连续仿真操作，通过仿真可知模型可以很好的模拟选岔工作，通过CPN TOOLS的Calculate State Space工具可进行模型的状态空间计算，同时自动保存状态空间报告。本文以图3所建立的变通进路的CPN模型为例对其状态空间报告进行分析。状态空间报告节点统计、有界性、家态性、活性、公平性的截图如图5—图7所示。

由图5可知，对变通进路选岔所建立的CPN模型所做的状态空间分析是全部的状态空间分析而不是部分的，由于有界性的状态空间报告内容较多，故只截取了其中的一部分，从图6所示报告中可知各节点库所的标识数目有界，由此可知所建立的网模型是安全的，由图7可知模型最终会终止在第441个节点，而该节点刚好是选岔结束的节点，说明选岔任务已完成，是符合功能逻辑的，通过多次仿真分析，发现系统都会终止在第441个节点上，这也验证了模型的家态性。报告中还可得到变迁的活性和托肯的活性，从报告中可知没有死变迁，也没有自动触发的变迁，这是因为选岔网络的工作信息来源于外部，每次执行完命令后均要等待下一次命令的到来，因此也不存在无限发生的序

列，这是与选岔网络工作的逻辑功能相符的。

图5 状态空间节点统计截图

图6 状态空间部分有界性截图

图7 状态空间家态性、活性、公平性截图

5 结论

本文在分析联锁系统选岔电路的基础上抽象出选岔网络的联锁条件，并根据这些联锁条件采用CPN对选岔网络建立形式化分析模型，同时采用cpn_tools 4.0.0对模型进行仿真及状态空间分析，分析证明所建立的模型能够很好的描述选岔网络的功能逻辑。

[1] 袁崇义. Petri网应用[M]. 北京：科学出版社，2013.

[2] 吴哲辉. Petri网导论[M]. 北京：机械工业出版社，2006.

[3] 袁崇义. Petri网原理及应用[M]. 北京：电子工业出版社，2005.

[4] 林瑜筠，王孝义等. 6502电气集中学习指导[M]. 北京：中国铁道出版社，2006.

[5] 宫杰，陈邦兴. 基于Petri网的联锁软件测评仿真建模[J].计算机应用与软件，2009，26（2）：11-13.

[6] 陈邦兴，吴芳美. 含过程和控制库所的层次化Petri网模型及应用[J]. 计算机应用，2005，25（6），1410-1413.

[7] 陈邦兴，吴芳美.铁路信号联锁逻辑形式化建模研究[J].铁道学报，2002，24（6）：50-54.

[8] 杜军威，徐中伟，王素梅.联锁逻辑模型的安全性分析[J].计算机工程及应用，2007，42（2）：1-4.

[9] M.S Durmus, M.T Soylemez, Railway Signlization and Interlocking Design via Automation Petri Nets, Proceedings of the 7th Asian Control Conference, HongKong, China. Augest 27-29,2009.

[10] Chen Xiang xian, HeYuLin, Huang hai. A component-based topology model for railway interlocking systems, Mathematics and Computers in Simulation 81 (2011) 1892-1900.

With detailed analysis of interlocking system switch selection circuit as a precondition, interlocking logic condition of switch selection network is abstracted, for which formalized verification model is established by adopting (colored Petri net CPN), simulation and status spatial analysis are made for the model established with CPN TOOLS, the results show that the working status of switch selection network is able to be well described by the established model.

Switch selection network; CPN; formalization; CPN TOOLS

U283

B

1007-936X(2015)02-0043-05

2014-06-09

陶 玲.重庆交通大学交通运输学院，硕士研究生，电话：18883861441；宋 军.重庆交通大学信息科学与工程学院，教授。