基于梯形逻辑的联锁系统形式化验证方法

摘要：铁路联锁系统设计通常采用梯形逻辑进行建模为了实现对铁路联锁系统进行形式化验证的目的，根据梯形逻辑的状态变迁语义，将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言，并将铁路联锁系统的安全需求表示为计算树逻辑（CTL），最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证

关键词：铁路联锁系统； 模型检测； 形式化方法； 梯形逻辑； NuSMV模型检测

中图分类号：TP311 文献标志码：A

0引言

在现代公共交通体系中，轨道交通系统具有不可替代的突出地位如何实现列车安全、快速、高效的运行，是摆在相关科研人员面前的一个突出问题铁路车站计算机联锁系统是铁路行车的重要设备，它所包含的相互制约关系和控制顺序往往十分复杂，所以联锁控制逻辑设计的正确性直接关系到列车的运行安全随着计算机技术在铁路信号系统的应用，安全问题显得越来越重要，传统的系统设计、分析和测试方法已经难以满足系统的安全需要近年来，基于离散数学的形式化方法发展迅速，为解决安全计算机系统设计开发的正确性问题提供了一条可能的途径[1]

作为一种图形化语言，由于其简单的逻辑关系、直观的表达方式，梯形逻辑在时序系统的设计领域得到广泛应用采用梯形逻辑对联锁控制逻辑进行设计，可以将联锁系统表述为一个迁移系统，通过这种基于梯形逻辑的迁移系统可以得到系统内部的状态空间而形式化验证方法就是对状态空间进行搜索，以期检测这个系统模型是否满足某些给定属性

本文针对梯形逻辑建模的特点，研究形式化验证的理论，尝试采用形式化方法对基于梯形逻辑的联锁控制系统设计模型进行验证，选取了计算树逻辑（Computational Tree Logic，CTL）符号模型检测方法对系统的设计模型进行形式化验证，最后选取实例进行模型到代码转化的应用，探索出基于梯形逻辑设计模型形式化验证的一整套方法

1模型检测

模型检测是一种验证系统属性的形式化方法，它从数学上完备地验证系统实现是否与规范一致模型检测通常采用状态空间遍历技术检测一个给定的计算模型是否满足用时态逻辑公式表示的特定属性模型检测对验证计算机系统的正确性具有传统方法无法比拟的优势，如全自动进行而无须人机交互，定位设计错误，系统建模的完整性等，尤其是对安全苛求系统，这种优势更为明显[2]

模型检测的主要思想是：将待检测的系统抽象为有限状态机，用时态逻辑描述系统应该满足的性质，然后遍历有限状态机的状态空间，对每个状态判断是否满足这些性质若不满足，给出一个不满足性质的状态序列[3]所以模型检测一般包含建模、规范、验证三个步骤

属性是与系统行为发生次序有关的时态属性，通常用时态逻辑表示时态逻辑是描述系统所处状态的性质以及状态间迁移序列的表达式，它可以方便准确地描述并发系统的重要性质，如安全性（safety）、活性（liveness）和公平性（fairness）安全性是指系统的正确性和互斥性，用于说明“某条件永远满足，或某危险事件永不发生”；活性是指系统的终止性、无活死锁性和响应性等，用于说明“某必需事件终将发生”；公平性是指系统的合理性，用于说明“某事件必须无限经常地发生”[3]CTL是首个用于模型检测过程的时序逻辑语言以一个有穷状态并发系统的Kripke结构的初始状态为树根，状态为节点，按各节点后继不同将Kripke结构展开，构成一棵计算树，树中任一条路径刻画系统的一次运行

模型检测工具如SMV、Spin等，以模型和属性公式为参数，通过执行验证算法自动搜索整个状态空间，以验证模型是否满足属性[4]算法的实现思想是通过穷举状态空间以计算出令公式为真的所有状态

2NuSMV分析软件

符号模型检测（Symbolic Model Checking， SMC）是一种用布尔公式隐式的表示系统状态集合和迁移关系，并在符号状态空间上进行搜索的技术对于要验证的CTL公式，通过对迁移关系进行相应的不动点运算，即可得到不动点的二叉决策图（Binary Decision Diagram， BDD）表示，用来进一步分析系统是否满足被验证性质[3]下面给出CTL模型检测的伪代码：

SMC过程中，子过程Check以有限状态机的BDD表示MBDD和CTL表达式f作为输入，输出结果是满足f的状态集合的BDD表示S0BDD表示初始状态集合S0的BDD

在符号模型检测方法的基础上，开发了模型检测工具SMV，而NuSMV是SMV的重新实现和扩展，是第一款基于BDD的模型检测器NuSMV被设计成一个开放式的系统，不仅开源而且很容易修改、定制和扩展它具有一个描述层次有穷状态并发系统的规范语言，并从系统规范中提取以BDD形式表示的迁移系统，然后用基于BDD的搜索算法确定系统是否满足CTL描述的被验证属性[6]

NuSMV分析软件以有限状态系统说明及其系统属性作为输入，若有限状态系统具有给定的属性，则输出true，否则输出false，同时提供一个违反规约的反例反例可以在不同的冗余层次或以可重用数据结构的方式来产生，并且可以被检查和操纵系统说明部分用NuSMV规定的SMV语言编程，属性部分则用CTL公式表达[7]

3梯形逻辑

梯形逻辑是一种图形化语言，由于其生成的梯形图呈阶梯状而得名，往往被用来对可编程逻辑控制器进行编程[8]梯形图中，假想左右两侧母线（左母线和右母线）之间有一个左正右负的直流电源电压，母线之间有“能流”从左向右流动依照梯形逻辑的这一特点设计系统模型，可以简化系统，直观地刻画出系统状态随时间顺序变换的迁移系统，实现对系统需求完全、正确和一致的描述由于其简单的逻辑关系、直观的表达方式，梯形逻辑在时序系统的设计领域得到广泛应用[9]

梯形逻辑是一个不断迭代的状态迁移过程，可以用每次执行后变量的不同状态来对系统的行为进行建模，故而引入自动机理论方法来对系统进行建模[7]用命题公式ΨP表示一个梯形逻辑，可以得到一个有限自动机

4基于梯形逻辑的联锁控制逻辑的模型检测

随着计算机技术的提高，计算机联锁系统变得越来越复杂，规模也越来越大复杂的系统很难设计开发，寻找错误和安全隐患也比较困难，一般的测试方法很难发现系统所有的设计故障，这会给轨道交通系统的安全、高效运行带来一定的安全隐患采用模型检测方法对车站联锁安全条件和联锁控制逻辑的设计进行验证，可以在很大程度上减少由系统开发人员造成的设计故障，提高系统的安全性

4.1用梯形逻辑设计联锁逻辑

联锁控制逻辑包括6个模块：操作命令形成模块、操作命令执行模块、进路处理模块、状态输入模块、表示输出模块以及控制命令输出模块其中，进路处理模块是联锁控制逻辑的核心，它的主要工作是在执行了进路搜索子模块对所办进路以形成进路表之后，对进路进行处理[11]梯形逻辑图可以很直观地表示出这种复杂的联锁逻辑关系，故如图1所示，选择一个简单的车站联锁站场图用梯形逻辑进行建模

对联锁控制逻辑的设计如下：进路操作输入后，进路搜索程序从站场数据库中选出进路，执行进路处理模块，共分为5个模块：区段检查和征用模块、道岔控制命令生成模块、进路锁闭模块、信号开放及关闭模块、区段解锁模块[12]

1）区段检查和征用模块要办理一条进路，首先检查该进路上所有区段是否空闲，是否已被征用如果该进路上所有区段都空闲，并且未被征用，则征用这些区段

2）道岔控制命令生成模块道岔有定位和反位两个工作位置，只有当道岔所在区段未锁闭时，道岔才能改变其工作位置道岔位置与进路以及进路始端信号机间的联锁关系如表1所示以道岔21为例，得到道岔转换的梯形图如图2所示

3）进路锁闭模块为了保证行车安全，信号机开放时，首先必须把进路中的所有区段置成锁闭状态，且把敌对进路锁闭在未建立状态，这种锁闭叫进路锁闭首先检查进路中的所有区段空闲、道岔位置正确，并且进路中的所有区段被该进路征用，当这些条件全部满足时，实现进路的锁闭

4）信号机开放及关闭模块在信号开放时需要满足以下技术条件：进路中道岔位置正确且道岔区段锁闭、进路中的所有区段空闲、敌对进路锁在未建立状态[13]列车一旦驶入进路，立即关闭信号机

5）区段解锁模块当进路锁闭后，进路上的所有区段实现锁闭实现三点检查法解锁区段：列车出清上一区段并解锁；列车出清本区段，本区段空闲；且在列车进入下一区段，下一区段被占用时，本区段解锁以区段12为例进行说明，得到梯形图如图3所示

4.2梯形逻辑的模型描述

梯形图的状态遍历特点与形式化验证的状态遍历特点不谋而合，在这里使用模型检测方法对梯形图进行验证首先采用NuSMV分析软件对用梯形图表示的系统进行建模，然后将道岔、进路、信号机之间的连锁关系用CTL表示出来，经过NuSMV分析软件的符号模型检测模块，可以确定基于梯形逻辑的设计模型是否符合计算机联锁控制逻辑的逻辑关系

NuSMV有两个很有用的表达式：init表达式和next表达式init表达式用于描述初始状态，next表达式用于描述转移关系NuSMV输入语言写的程序常被称为smv程序所以在将梯形图模型转化为smv程序时：首先将梯形图中涉及的状态变量进行声明；然后就可以将梯形图的每一个梯级描述成为一个next表达式，即当同一梯级的能流所经过的元件对应的变量状态满足时，输出元件对应变量的下一状态改为相应状态这样，利用NuSMV语言中的next表达式可以准确地描述梯形图表示的有限状态系统的逻辑关系，生成状态变迁关系的模型[14]

根据图2，可以将道岔21工作位置转换的梯形逻辑转化为smv代码如下：

4.3梯形逻辑的模型检测

4.3.1安全属性CTL表达

联锁控制逻辑的安全性是指系统的正确性和斥性，用于说明“坏事情永远都不会发生”[15]，主要有以下两种情况：

1）道岔与进路之间的联锁关系

道岔与进路之间的联锁关系在进路选排时进行条件设定在获取安全性时，可以用道岔与信号机之间的联锁关系表示[16]，见表2

用CTL公式表示只有道岔位置正确，信号机才能开放：

2）进路与进路之间的联锁关系

办理进路时，需要占用同一区段的进路为敌对进路，进路间的敌对关系见表3

4.3.2活性CTL表达

联锁控制逻辑的活性是指系统的终止性、无活死锁性、保证服务性和响应性等，用于说明“好事情最终会发生”，有以下两种情况：

1）每个信号机都会开放：

2）设置进路，可能会开放相应的信号机，但并不是一定开放

这样，用NuSMV可以实现对联锁系统的梯形图的建模，生成一个完整的迁移系统，同时，用CTL可以很好地表示获得的联锁关系属性，利用NuSMV自身提供的功能从模型检测的角度实现安全验证

4.3.3模型验证结果

根据图4所示的检验结果可以看到：采用NuSMV验证工具对上述基于梯形逻辑的车站联锁系统设计模型进行模型监测，全部属性的验证结果均为true，即用梯形逻辑对计算机联锁控制逻辑的设计符合系统的安全规范

5结语

模型检测能避免建立复杂的证明过程，同时能在不满足性质时提供反例，这样可以有效地验证模型，避免设计型故障采用模型检测方法对用梯形逻辑设计的联锁控制逻辑系统模型进行验证，可以保证系统设计模型的正确性和可靠性，这种自动化验证技术可以大大减少人力资源的浪费但模型检测在对梯形逻辑表示模型的验证中也存在一些问题有待解决：1）模型检测的主要缺陷就是状态空间爆炸问题，但是解决状态空间爆炸的技术相对于实际系统规模仍有差距；2）模型检测工具要求使用者用特定的系统规范语言刻画梯形逻辑描述的迁移系统，所以使用难度较大

今后，希望能通过从梯形逻辑到模型检测规范语言的自动转换，实现高效的自动化验证技术，最终目的是能在设计阶段较早地获得安全性能估计

参考文献：

[1]燕飞. 轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D]. 北京：北京交通大学，2006：6-20.

[2]唐涛，徐田华，赵琳. 列车运行控制系统规范建模与验证[M]. 北京：中国铁道出版社，2010：25-110.

[3]边计年，薛宏熙，苏明，等. 数字系统设计自动化[M]. 北京：清华大学出版社，2005：327-380.

[4]HAXTHAUSEN A E. An introduction to formal methods for the development of safetycritical applications[D]. Lyngby： Technical University of Denmark， 2010：6-19.

[5]NING N， ZHANG J， GAO X Y. Formal verification for the solution of signed directed graph fault diagnosis via symbolic model checking [J]. Chinese Association of Automation，2010，39（4）：423-429.

宁宁，张骏，高向阳.基于符号模型检测的符号有向图故障诊断解形式化验证[J].信息与控制，2010，39（4）：423-429.

[6]CAVADA R， CIMATTI A. NuSMV 2.5 user manual [K/OL]. [2013-02-12]. http：//nusmv.fbk.eu/NuSMV/userman/v25/nusmv.pdf.

[7]ERIKSEN L E. Verification of safety properties for relay interlocking systems [EB/OL]. [2013-02-16]. http：//etd.dtu.dk/thesis/266717/ep10_57_net.pdf.

[8]JAMES P. SATbased model checking and its applications to train control systems [EB/OL]. [2013-02-20]. http：//www.cs.swan.ac.uk/～csmarkus/ProcessesAndData/Papers/james10a.pdf.

[9]JAMES P， ROGGENBACH M. Designing domain specific languages for verification： first steps [C/OL]// ATE11： Proceedings of the 2011 Australian Tourism Exchang. 2011： 40-45. http：//www.cs.swansea.ac.uk/～csmarkus/ProcessesAndData/Papers/james11a.pdf.

[10]JAMES P， ROGGENBACH M. Automatically verifying railway interlockings using SATbased model checking [J]. Electronic Communications of the EASST， 2010， 35（2010）：3-9.

[11]燕飞， 唐涛. 计算机联锁控制逻辑的模型检验方法[J]. 铁道通信信号，2009，45（5）：26-29.

[12]LI J， CHEN S. Design of software based on railway transportation interlocking control testing system [J].Railway Computer Application， 2011， 20（3）：46-49.

[13]HEI X， OUYANG N. The scheduling strategy of concurrent request in distributed railway interlocking system [J]. ICIC Express Letters， Part B： Applications， 2011， 2（1）：43-48.

[14]张军林. NuSMV模型验证器实现分析[D]. 广州：中山大学，2010： 19-23.

[15]HAXTHAUSEN A E. Automated generation of safety requirements from railway interlocking tables [C]// ISoLA12： Proceedings of the 5th International Conference on Leveraging Applications of Formal Methods， Verification and Validation： Applications and Case Studies， LNCS 7610. Berlin： SpringerVerlag， 2012： 261-275.

[16]ZAFAR N A， KHAN S A， ARAKI K. Towards the safety properties of moving block railway interlocking system [J]. International Journal of Innovative Computing， Information and Control， 2012， 8（8）： 5677-5690.