基于模型检测的安全分析技术在轨交信号系统的应用①

徐美芳， 陈邦兴， 于小飞

(同济大学电子与信息工程学院，上海201804)

0 引言

近年来，随着我国城市发展的需要，建设城市轨道交通系统成为解决城市交流、缓减交通压力的重要手段.信号系统作为保证列车安全、正点、快捷、舒适、高密度不间断运行的重要技术装备在轨道交通系统中有着举足轻重的地位.它是保障城市轨道交通系统有计划、有组织、安全、高效运行的关键系统，所以，提高信号系统的安全性对于整个轨道交通系统的安全运行具有极大地影响［5］.

实践发现，传统的安全分析法非常依赖安全分析人员的经验和能力.受人类认知能力的限制，常常难以预测系统所有可能的行为(包括正常和异常行为)，容易造成疏漏或误判某些系统的失效状态.例如，对于故障树分析而言，不同的安全分析人员对同一个系统所构建的故障树的差异度很大，而且构建的故障树和系统之间的一致性也很难保证.即使故障树和系统的一致性能够达到，由于安全分析所使用的模型是非形式化的，它的分析结果也不可能一定是完整、正确.而且，随着系统复杂性的加大，系统所包含的部件越来越多，单靠工程技术人员手工完成安全分析的困难度大大增加，尤其对轨道交通等安全苛求系统，传统安全分析技术渐渐不能胜任，所以必须研究一种更自动、更客观、更全面、更系统化的方法来满足当前安全分析的需求.为此，本文将计算机学科的形式化验证中的模型检测技术引入到复杂的轨道交通系统的安全性评估中.

基于模型检测的安全分析新技术，利用遍历算法，不仅可以从数学上确保搜索出系统的所有可达状态，又可以利用模型检测工具，自动实现安全分析，降低对分析人员的依赖，同时降低了成本.

本文提出了一种基于模型检测的安全分析新技术，并研发了集FTA和FMEA于一体的安全分析工具，利用此工具可以实现自动识别导致某顶事件发生的最小割集，达到传统故障树分析的目的，同时省去建立故障树的过程，降低了对分析人员的依赖，并缩减了分析成本和时间.最后以轨道交通信号系统为例，把此工具得到的结果和权威人士传统故障树分析的结果对比，说明了此方法的过程及正确性.

1 基于模型检测的安全分析技术

1.1 模型检测技术简介

模型检测技术最早由Clarke、Emerson等人于1981年分别提出，可从数学上完备地证明或验证所实现的系统是否与规范一致.模型检测首先将系统模型转化为一个有限状态机，如Kripke结构.再将描述系统特性的系统规范表示为一组时态逻辑公式，如计算树逻辑(CTL).最后使用检测工具验证状态转移关系是否满足逻辑公式，如果不满足，检测工具将会给出一个反例，其示意图如图1所示:

图1 模型检测示意图

最初发展的显示模型检测技术在描述系统状态及其转移结构时容易出现状态爆炸问题，而符号模型检测技术的引入，大大缓减了状态空间爆炸问题，本文也采用了符号模型检测技术［2］.

1.2 基于模型检测的安全分析技术流程

本文提出的基于模型检测的安全分析新技术，目的在于自动识别导致某顶事件发生的最小失效组合(即最小割集)，达到传统故障树分析的目的.该方法的流程图如图2所示［10］.

图2 基于模型检测的安全分析流程图

1.2.1 系统模型扩展

系统模型扩展是向系统标称模型中的部件状态注入故障模式的过程.其故障模式注入机制如图3所示.

左边为系统标称模型的一个功能模块“A”，它有两个输入信号和一个输出信号.为了扩展此模型，在模块“A”中注入两个故障模式FM1和FM2.右边为扩展模型，它包括一个功能模块“A_Extended”，此模块由标称系统模型中的模块“A”和两个额外的模块“A_FM1”、“A_FM2”组成，这两个模块分别描述了两个注入到模块“A”中的故障模式.例如，假设FM1为输出一直为零的故障模式，则无论输入值是多少，A_FM1模块的输出将永远为0.对于扩展模型来说，它的输入还是为原来标称系统模型的输入，输出信号则由一个多路复用器决定.而多路复用器的输入来自模块A、A_FM1和A_FM2的输出，输出结果由FM信号控制，此信号被称为失效模式变量，是系统三种状态{OK，FM1，FM2}的集合，决定多路复用器的最终输出.如果FM信号为OK，则认为系统没有发生故障，标称系统模型中的模块A的输出即为扩展模型最终的输出，其他同理.

1.2.2 安全分析工具

基于符号模型检测技术，本文研发了一个安全分析工具，它可以同时实现故障树分析和失效模式与影响分析.它的开发流程主要包括两部分:构建语言分析器和实现基于符号模型的前向搜索算法.

1.2.2.1 语言分析器

为了利用符号模型检测技术，需要将自定义的扩展模型状态及其变迁关系的描述语言接收成有序二叉判决图(OBDD)形式.本文利用Lex和Yacc工具构建语言分析器.Lex为词法分析器.它使正则表达式匹配输入的字符串并且把它们转换成对应的标记.Yacc为语法分析器.它使用特定的语法规则以便解释从Lex得到的标记并且生成一棵语法树.通过Lex和Yacc的结合，同时调用处理二叉决策图的CUDD开发包，可以将扩展模型的状态及其变迁关系转换成OBDD形式，提高后续算法实现的效率.

1.2.2.2 基于符号模型检测的前向搜索算法

将扩展模型的状态及其变迁关系构建成OBDD之后，就可以利用模型检测的前向搜索算法找出故障树的最小割集.其算法如下所示:

Function FTA－Forward(M，TLE)1 M:=Extend(M，RO)2 Reach:I;3 Front:=I;do 5 temp:=Reach;4 While(Front!=null));7 Front:=Reach emp;6 Reach:=Reach∪ fwd_img(M，Frong 8 end While ;);10 MSC:=Minimize(CS);9 CS:=Proj(f，Reach ∩Tle

算法的输入是系统的Kripke结构M和满足顶事件的状态集合TLE，Extend(M，R0)是系统注入故障模式后的扩展模型，R0表示扩展模型的状态变迁关系，包括正常工作模式变量和失效模式变量两部分变迁.变量Reach用于累积系统可达状态，变量Front用于保持搜索的边界，这两个变量初始化都为系统的初始状态，包括正常工作模式变量和失效模式变量两部分.这个算法的核心是应用像操作符计算可达状态，直到得到系统的固定点为止，此时边界状态为空.上述得到的状态和满足顶事件的状态取交集，再投影到故障变量上可以得到系统的割集.简单的说，就是将扩展模型和满足故障树顶事件的状态作为输入，搜索状态变迁系统的每一条路径，直到到达满足顶事件的状态，在搜索过程中，记录每一条路径中发生的故障模式变量.每一条到达顶事件状态的路径中存在的失效模式变量组成的一个集合就可以构成系统故障树的一个割集，所以，基于符号模型检测的前向搜索算法通过直接对已注入故障模式的扩展模型进行全局搜索得到系统的所有割集，而不需要针对某个顶事件建立对应的复杂故障树.得到系统的最小割集就可以进行风险分析和危害识别了，每个最小割集都是顶事件发生的一种可能，有几个最小割集，顶事件的发生就有几种可能，最小割集越多，系统就越危险.而且，最小割集能直观地、概略地看出，哪些事件发生最危险，哪些稍次，哪些可以忽略，以及如何采取措施，使事故发生概率下降，提高系统的安全性.

图3 故障注入机制

1.2.2.3 工具建模语言

这里将介绍此工具建模语言的语法规则.首先定义一些标示符:

VAR:用于标记描述系统所需用到的正常状态变量;FVAR:用于标记描述系统所需要用到的故障变量;TLE:用于标记系统的顶事件;Initial State:用于标记系统的初始状态;TRANS:用于标记系统的变迁过程;

变量的命名可以用英语字母或者单词，下划线，数字的组合来表示.变量的数据类型可以是布尔，整型，枚举类型.定义形式如下所示:FVAR标示符类似于VAR.

?

标示符TRANS表示以下描述的是系统的整个变迁过程.在描述变量的变迁关系时常用的关键字有case和next.case表示变量变迁的各种情况，系统最终变迁是全部变量各种变迁的组合.next表示一个变量的下一个状态的取值.其基本的表达式规格如下所示:

?

关键词next中，如果变量满足一定的条件则发生变迁，若不满足则保持原值.条件一般可以用状态中其他变量之间的与或非，蕴含或者等价操作来表示，这些操作分别用符号＆，|，～，－＞，＜－＞.

2 实例应用

在高速发展的轨道交通系统中，作为轨道交通运行的神经中枢，信号系统发挥着越来越重要的作用，但是其发展必须以保证行车安全为前提.只有信号系统的安全得到保障和提高，整个轨道交通系统的安全性才能得到保障和发展，所以本文以信号系统为例，利用基于符号模型检测的安全分析工具，对其安全性进行分析［11］.

2.1 信号系统的建模

在轨道交通系统中，最主要的一个危害是两辆列车占用同一个轨道区段.一旦发生这种情况，发生事故的概率就大大提高了.而信号系统在预防此类危害发生时发挥了举足轻重的作用.一个简单的信号系统模块框图如图4所示:

图4 信号系统的模块图

此信号系统主要包括以下几个模块:列车检测模块，主要检测轨道区段是否被某列车占用，并把信号发送给联锁模块;联锁模块，主要用于计算列车检测模块和临近联锁模块发来的信息，并把结果发送给信号灯模块;信号灯模块，根据联锁模块发来的信息，决定显示相应的信号灯;司机模块，根据信号灯的显示，做出相应的列车操作.若信号灯显示为红色，则采取常规制动;若信号灯显示为绿色，则列车通过;ATP模块，主要是一个辅助作用，当信号灯显示红色时，司机由于某种原因没有采取常规制动，此时ATP系统应该采取紧急制动，迫使列车停下.

为了扩展此信号系统，本文对每一个模块都注入了一个故障模式，其扩展模型如图5所示，且各个模块用相应的英文表示以简化后续建模［7］.

图5 扩展模型的系统框图

在使用安全分析工具之前，首先需要对信号系统的扩展模型进行形式化建模，将其初始状态和变迁关系描述成语言分析器能够接受的代码，其初始状态的建模如下所示:

?

正常工作模式变量的变迁关系如下所示:

?

故障模式的变迁则需要遵循如下规则:故障变量的状态有TRUE和FALSE两种情况.在TRUE状态下，即故障发生，则下一状态始终为TRUE;在FALSE状态下，即故障未发生，则下一状态可是FALSE或TRUE.所以，其变迁关系如下所示:

?

2.2 安全性分析

完成信号系统扩展模型的形式化建模后，本文利用基于模型检测的安全分析工具自动生成了导致两辆列车占用同一个轨道区段这一顶事件发生的最小割集.使用“TLE:OC=1＆MB=0＆EB=0”描述顶事件，将顶事件和形式化模型输入到安全分析工具中，通过状态遍历一共生成了5组最小割集，如表1所示.

表1 信号系统的最小割集

最小割集显示:当列车检测模块(TD)单独发生故障时，即如果轨道区段有列车，但是列车检测模块发送了轨道区段无车的信号，就会导致顶事件的发生.同理，当联锁模块(In)和信号灯模块(Sig)各自单独发生故障时，也会导致顶事件发生，当司机模块(Dr)和ATP模块一起发生故障时，也会导致顶事件发生，当正常制动模块(MB)和紧急制动模块(EB)一起发生故障时，也会导致顶事件发生.

为验证文本方法的正确性，上述系统由约克大学所建立的故障树如图6所示:

图6 信号系统传统故障树

其中，1表示顶事件，两辆列车占据同一个轨道区段;2表示信号灯不正确;3表示信号开放正确，但是列车没有根据信号进行相应操作;4表示信号灯本身硬件的错误;5表示信号命令错误;6表示刹车失效;7表示没有踩刹车的命令;8表示信号信息在传输中反转;9表示联锁系统允许冲突的信号;9表示常规制动刹车失效;10表示紧急制动刹车失效;11表示司机没有常规制动;12表示ATP没有紧急制动;13表示联锁系统发生联锁错误;14表示列车检测模块错误;15表示从另一个联锁发来的信息是错误的;

将上述故障树经过分析得到的最小割集与文本得到的最小割集完全相同，表明本文方法可以自动实现安全分析的目的.

3 结束语

本文研发了一个基于符号模型检测的安全分析工具，利用语言分析器，将系统描述语言转换成有序二叉决策图(OBDD)结构，并结合符号模型检测技术，用前向搜索算法按照逻辑表达式描述对系统状态进行搜索检验，自动生成与传统故障树分析结果一致的最小割集，并以轨道交通的信号系统为例说明此方法的正确性和可行性.此方法可以自动实现故障树分析，同时省去建立故障树的过程，降低了对分析人员的依赖，并缩减了分析成本和时间.随着模型检测方法的不断发展，其能够处理的状态数量可基本满足复杂系统安全性分析的需求，因而基于模型检测的方法也逐渐在安全苛求领域发挥越来越大的作用.

［1］Bryant，R.E.Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams［J］.ACM Computing Surveys，1992，24(3):293－318.

［2］Clarke.Model Checking［J］.Cambridge，2002.

［3］A.Thums and G，Schellhorn.Model Checking FTA.Augsburg，2003.

［4］Marco Bozzano，Alessandro Cimatti，Francesco Tapparo.System Fault Tree Analysis for Reactive System.Italy，2003.

［5］燕飞，唐涛.轨道交通信号系统安全评估方法研究［J］.中国安全科学学报，2005，15(10).

［6］Ethan L.Schreiber.A CUDD Tutorial［Z］.The University of California，Los Angeles，2008.

［7］郦萌，吴芳美.铁路信号可靠性安全性理论及证实［M］.北京:中国铁道出版社，2008:55－90.

［8］Thomas Ball，SriramK.Rajamani.Bebop:vA Symbolic Model Checker for Boolean Programs.Microsoft Research，2009.

［9］Pierre Bieber，Charles Castel，and Christel Seguin.Combination of Fault Tree Analysis and Model Checking for Safety Assessment of Complex System.France:31055 Toulouse Cedex，2010.

［10］Marco Bozzano，Adolfo Villafiorita.Design and Safety Assessment of Critical System .USA:Taylor and Francis Group，2011.

［11］Oleg Lisagor.Andrew Rae，Mark Nicholson.Introduction to System Safety Engineering .York University，2011:87 －143.