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

《基于梯形逻辑联锁系统形式化验证方法》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、基于梯形逻辑联锁系统形式化验证方法　　摘要：铁路联锁系统设计通常采用梯形逻辑进行建模为了实现对铁路联锁系统进行形式化验证的目的，根据梯形逻辑的状态变迁语义，将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言，并将铁路联锁系统的安全需求表示为计算树逻辑（CTL），最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证关键词：铁路联锁系统；模型检测；形式化方法；梯形逻辑；NuSMV模型检测中图分类号：TP311文献标志码：A0引言在现代公共交通体系中，轨道交通系统具有不可替代的突出地位如何实现列车安全、快速、高效的运行，是摆在相关科研人员面前的一个突出问题铁路车站计算机联锁系

2、统是铁路行车的重要设备，它所包含的相互制约关系和控制顺序往往十分复杂，所以联锁控制逻辑设计的正确性直接关系到列车的运行安全随着计算机技术在铁路信号系统的应用，安全问题显得越来越重要，传统的系统设计、分析和测试方法已经难以满足系统的安全需要近年来，基于离散数学的形式化方法发展迅速，为解决安全计算机系统设计开发的正确性问题提供了一条可能的途径[1]13作为一种图形化语言，由于其简单的逻辑关系、直观的表达方式，梯形逻辑在时序系统的设计领域得到广泛应用采用梯形逻辑对联锁控制逻辑进行设计，可以将联锁系统表述为一个迁移系统，通过这种基于梯形逻辑的迁移系统可以得到系统内部的状态空间而形式化验证方法就

3、是对状态空间进行搜索，以期检测这个系统模型是否满足某些给定属性本文针对梯形逻辑建模的特点，研究形式化验证的理论，尝试采用形式化方法对基于梯形逻辑的联锁控制系统设计模型进行验证，选取了计算树逻辑（ComputationalTreeLogic，CTL）符号模型检测方法对系统的设计模型进行形式化验证，最后选取实例进行模型到代码转化的应用，探索出基于梯形逻辑设计模型形式化验证的一整套方法1模型检测模型检测是一种验证系统属性的形式化方法，它从数学上完备地验证系统实现是否与规范一致模型检测通常采用状态空间遍历技术检测一个给定的计算模型是否满足用时态逻辑公式表示的特定属性模型检测对验证计算机系统的正

4、确性具有传统方法无法比拟的优势，如全自动进行而无须人机交互，定位设计错误，系统建模的完整性等，尤其是对安全苛求系统，这种优势更为明显[2]13模型检测的主要思想是：将待检测的系统抽象为有限状态机，用时态逻辑描述系统应该满足的性质，然后遍历有限状态机的状态空间，对每个状态判断是否满足这些性质若不满足，给出一个不满足性质的状态序列[3]所以模型检测一般包含建模、规范、验证三个步骤属性是与系统行为发生次序有关的时态属性，通常用时态逻辑表示时态逻辑是描述系统所处状态的性质以及状态间迁移序列的表达式，它可以方便准确地描述并发系统的重要性质，如安全性（safety）、活性（liveness）和公平

5、性（fairness）安全性是指系统的正确性和互斥性，用于说明“某条件永远满足，或某危险事件永不发生”；活性是指系统的终止性、无活死锁性和响应性等，用于说明“某必需事件终将发生”；公平性是指系统的合理性，用于说明“某事件必须无限经常地发生”[3]CTL是首个用于模型检测过程的时序逻辑语言以一个有穷状态并发系统的Kripke结构的初始状态为树根，状态为节点，按各节点后继不同将Kripke结构展开，构成一棵计算树，树中任一条路径刻画系统的一次运行模型检测工具如SMV、Spin等，以模型和属性公式为参数，通过执行验证算法自动搜索整个状态空间，以验证模型是否满足属性[4]算法的实现思想是通过穷

6、举状态空间以计算出令公式为真的所有状态2NuSMV分析软件符号模型检测（SymbolicModelChecking，13SMC）是一种用布尔公式隐式的表示系统状态集合和迁移关系，并在符号状态空间上进行搜索的技术对于要验证的CTL公式，通过对迁移关系进行相应的不动点运算，即可得到不动点的二叉决策图（BinaryDecisionDiagram，BDD）表示，用来进一步分析系统是否满足被验证性质[3]下面给出CTL模型检测的伪代码：SMC过程中，子过程Check以有限状态机的BDD表示MBDD和CTL表达式f作为输入，输出结果是满足f的状态集合的BDD表示S0BDD表示初始状态集合S0的BD

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