张梦云
郑州盛林人力资源有限公司 河南省郑州市 450000
摘要：计算机连锁软件是一种有效的验证计算机连锁软件能否满足某些安全属性的形式验证。本文介绍了一种基于模型检验的方法，对联锁系统模型和安全属性模型的建立方法进行讨论，并结合具体的站场实例，对信号开放功能进行了模型描述和验证，结果表明，该方法在计算机连锁系统中的应用是可行的。
关键词：计算机联锁；形式化验证；模型检验
中图分类号：W757文献标识码：A
１形式化验证
传统的联锁测试方法在某些情况下可以验证系统具有特定的安全属性，但仅限于测试场景，无法验证系统在任何情况下都能满足该安全属性。以联锁常用的布尔变量为例，如果系统由多个布尔变量组成，就会有2?种布尔变量，如果这个系统在每个案例中都经过测试，那显然是不可行的。为了保证系统的安全性和可靠性，在航空航天、半导体芯片等设计领域都采用了形式化方法，形式化验证方法包含定理证明和模型检验。其中，定理证明采用的是逻辑公式来表示验证的系统和形式的，这种方法与数理逻辑紧密结合，通常需要与用户进行交互，要求用户提供最具有创造性的验证工作，因此其自动化程度比较低、验证成本又很高，难以用于大规模系统的验证。而模型检验则是搜索模型的状态空间，通过遍历状态空间确认这个系统模型具有哪些特性。其优点是可以自动执行，当系统的性能不能满足时，可以给出反例。因而在工业界，模型检验的方式比定理证明会更加受到追捧。
２模型检验
使用模型检验方法对系统进行验证的过程主要包括系统模型建立、安全属性模型建立和验证三个步骤。
模型检验首先应该建立系统模型，即将被检测的系统转化为模型检验工具可以接受的形式；其次是建立安全属性的模型，即对系统所必须满足的安全属性进行形式化的描述；最后将系统模型和安全属性模型输入到模型检验工具中，验证系统是否具有所定义的安全属性[1]。
模型检验的困难在于它所能检测的是有限状态模型。这对于通用软件来讲，要有一个从任意状态到有限状态的过程，这种模型的状态空间还可能会有爆炸的问题出现。有界模型检验（BMC）是通过把有限状态机和LTL逻辑验证规范否定形式，编码成可以满足性问题（SAT）的实例，然后由解决SAT的相关工具去求解。如果有解决办法，就产生反例；如果没有解决办法，则系统运行至设定的边界阈值K后就会停止运行，也就是说系统到这个阶段是安全的。BMC能够使模型检验的变量数提高到一个数量级以上，并且易于获得长度最短、最简单明了的反例，有利于设计人员找出问题的所在。但是有界模型并没有解决状态空间爆炸的问题，而是通过只验证一部分状态空间的方式，而缩小了验证的范围，使得验证速度更快，查找的反例规模更小。
K—induction作为一种基于可满足性判定的验证技术，已经逐渐应用于软件分析与验证当中.K—induction是若不变式在程序执行路径之前k步都是成立的，然后证明它在k+1步也是成立的。而计算机联锁软件具有离散时间和顺序执行的特点，首先验证了在初始周期和k周期内可达的状态都满足一定的安全属性，再验证系统在k+1个周期内也满足该安全属性，从而验证了系统在任何周期都满足这一安全属性。因此，有界模型检验可以快速地发现反例，设计人员可以利用反例检验找出修正系统或建模时存在的问题，在所发现的问题都得到修正之后，再通过K—induction来实现模型检验的完备性。然后将该验证方法实际应用到计算机联锁系统时，由于模型检验的空间有限，同时要求模型检验要在有限的时间内完成，所以在建模时也要运用抽象技术，去掉无关紧要的细节。基于模型检验的特点，对于只给出了部分属性的系统，通过检测也可以得到关于已经知道的部分正确性的有效资源。
因此，基于系统的安全属性，只对安全属性中涉及到的系统相关内容进行建模，忽略与安全需求无关的设计细节，从而简化系统模型，提高验证的效率[4]。
３联锁的形式化验证
３.1系统模型的建立
计算机联锁软件通常由以下几部分构成。
（1）站场图形：包含了信号机、轨道电路和道岔等设备的拓扑连接关系。
（2）特定配置：包含了车站所有信号设备的类型、特性，以及进路表等静态数据信息。
（3）联锁逻辑：包含了进路、道岔、信号机之间的联锁功能的软件控制逻辑。
在通用系统建模的过程中，采用面向对象的方法，设计了道岔、进路、信号机、轨道电路等基本父类，在其中定义了各种类型设备的基本属性，并且可被子类继承，在子类中根据设备的具体类型对基本属性进行细化和增加。
通用系统模型建立完成后，实际的连锁软件可以通过与联锁逻辑中的变量，以及站场图形、进路表等输入文件中各变量之间的对应关系，将实际联锁软件自动转换成验证工具能够识别的形式。这种系统模型具有较高的可读性，易于信号专业人员理解和查找问题[2]。
3.2安全属性模型的建立
模型检验还应该对系统安全属性进行规范性表示，阐明系统必须满足的属性。需要注意的是，形式化验证只能确保系统满足规范表达的安全属性，而安全属性的语义无法验证，所以需要人工保证系统在意义上是正确的。
谓词逻辑很接近于自然语言，用它很容易被人们理解和接受它所表达的问题。例如，对于自然语言描述的一条联锁安全属性：“信号开放，则以该信号为始端的进路中的道岔应在规定位置”。把它进一步的向形式化描述方法靠拢，修改为“如果一个信号开放，就会有一条以它为始端的进路中的道岔均在规定位置”。最终它的形式化表达为：其中ALL和SOME都是量词，“—＞”是逻辑词“蕴含”，表示“如果……，那么……”的语义，因此A—＞Ｂ表示如果A为真，则Ｂ为真。那么上述表达式的含义为：对于所有的信号机，如果信号是开放的，那么必须有一条以信号开头的路径，并且路径中的所有道岔都在该路径所指定的位置。
在验证工具中，对某实际联锁站的数据进行了验证程序。通过对站场中的43架信号机的安全性能验证，表明该系统在任何状态下都能够满足“信号开放，则以该信号机为始端的进路中的道岔应在规定位置”的安全需求[3]。
4结论
计算机联锁系统随着站场复杂性的增加和软件规模的扩大，模型检验作为一种自动形式验证方法，可以通过选择合适的验证手段，满足联锁软件的形式化验证需求，为软件的安全性提供验证依据，提高安全可靠性。由于布尔代数本身在复杂的数学理论问题中起着基础性的作用，因此用基本逻辑的布尔代数描述的联锁系统在各种过程中相对容易解决，也更容易实现形式化验证。但形式化验证在很大程度上取决于系统模型的形式，系统设计方法一旦确定，就在很大程度上决定了形式化验证的难易程度，因此在设计阶段，应尽早地进行形式化验证，这样更有利于进行核查，从而确保联锁系统的安全性，并及时纠正在验证中发现的设计问题。
参考文献：
[1]赵志熙.计算机联锁系统技术[M].北京:中国铁道出版社,1999.
[2]燕飞，唐涛．计算机联锁控制逻辑的模型检验方法［J］.铁道通信信号,2009,45（5）：26—29.
[3]何文卿．6502电气集中电路［M］．北京：中国铁道出版社，2007．
[4]于丽贞，徐中伟．基于梯形逻辑的联锁系统形式化验证方法［J］.计算机应用，2013，33(12):3419－3431．