摘要：铁路车站计算机联锁系统是一种典型的安全苛求系统，重点是保障系统运营安全。对系统安全进行了分析，建立UML场景时序图，以此为基础建立系统的标号迁移模型，通过模型检测对系统进行安全性验证与分析，设计了系统的安全模型，为安全苛求系统的安全性分析与验证评估提供了一个完整的技术框架，具有理论及实际价值。
关键词：安全性分析；形式化方法；模型检测
中图分类号：TP309
文献标识码：A
文章编号：16727800（2017）004019103
0引言
铁路车站计算机联锁系统[1]属于安全等级为SIL4的安全系统，是一种典型的安全苛求系统[2-3]。系统进路子模块担负着确保行车安全的重要职责，各功能部件之间关系和控制逻辑十分复杂，不正确的联锁逻辑关系会导致列车相撞的灾难性事故，是安全要求最高的子模块之一。 关于铁路车站计算机联锁系统安全性的研究较多，文献[4]采用Event-B方法对道岔控制电路的安全规范进行了形式化模型描述和验证分析，在系统开发早期及时发现设计错误或漏洞；文献[5]采用有色Petri 网对联锁进路控制建立形式化分析模型，通过CPN Tools对模型的状态空间进行仿真分析，从而验证了系统形式化建模的正确性；文献[6]以基本进路为例，提出基于场景分析的系统形式化模型生成方法，该方法从安全质量方面改善了安全苛求软件的设计；文献[7]采用Rhapsody工具对铁路联锁系统的UML模型进行功能模拟，根据模拟结果分析是否存在不安全进路；文献[8]通过基于进程控制的EVALPSN程序模拟器对铁路联锁系统安全性进行模拟验证；文献[9]利用Z语言对移动闭塞情况下的联锁系统进行形式化建模；文献[10]采用VDM工具对丹麦铁路联锁系统进行形式化描述；文献[12]采用符号化模型检验策略和相应软件SMV对铁路计算机联锁控制逻辑设计进行形式化建模与验证。以上研究对铁路车站计算机联锁系统的形式化建模、安全性设计、功能模拟与仿真等具有较好的理论指导意义，但没有从系统需求分析、形式化建模、安全分析到系y安全性设计模型方面提供完整的技术框架。 本文在前期研究成果[6， 13]基础上，对铁路车站计算机联锁系统的进路建立子模块，建立系统安全性设计模型，为系统安全性分析与验证提供了一个完整的技术框架。
1铁路车站计算机联锁系统形式化建模
在铁路车站计算机联锁系统中，从车站值班人员开始办理进路到信号机开放，分为6个阶段：①操作阶段：值班人员按规定操作办理进路以确定进路的范围、方向、性质（列车或调车）以及特征（基本进路、变更进路等）；②选路阶段：根据已确定的进路范围，选出一条相应的进路；③道岔转换阶段：检查已选出的道岔实际位置是否符合进路要求，不相符时应将其转换到实际位置；④一致性检查阶段：检查进路中的各个道岔位置是否符合进路要求，为锁闭道岔作准备；⑤进路锁闭阶段：在道岔位置正确、进路空闲、未建立敌对进路的条件下，将道岔和进路锁闭，为信号开放作准备；⑥开放信号阶段：开放信号，允许列车或车列驶入进路。 采用UML时序图描述列车进路建立的场景如图1所示。图1中矩形框为交互框，操作符par表示并发，操作符alt表示选择，框中的虚线是分隔线，各消息含义如表1所示。
建立UML时序图场景各部件对象，如User、ILController、Switch、Section、Signal的标号迁移系统模型状态及迁移关系描述如下，其中迁移条件stop表示暂时终止进路建立，其余迁移条件具体含义见表1。
User=Q0， Q0=（routeSelect -> Q1）， Q1=（routeSetUpOK -> Q0|routeSetUpFailed -> Q2）， Q2=（stop -> Q0） ILController = Q0， Q0=（routeSelect -> Q1）， Q1=（conflictRouteCheck -> Q2 |routeCheck -> Q15 |switchCheck -> Q20）， Q2=（conflictRouteExisting -> Q3|noConflictRouteSetUp -> Q5）， Q3=（routeSetUpFailed -> Q4）， Q4=（stop -> Q0）， Q5=（switchCheck -> Q6）， Q6=（switchCorrect -> Q7），Q7=routeCheck -> Q8）， Q8=（routeEmpty -> Q9）， Q9=（switchLocked -> Q10）， Q10=（routeLock -> Q11）， Q11=（routeLocked -> Q12）， Q12=（signalClear -> Q13）， Q13=（signalCleared -> Q14）， Q14=（routeSetUpOK -> Q0）， Q15=（routeOcupied -> Q3 |routeEmpty -> Q16）， Q16=（switchCheck -> Q17）， Q17=（switchCorrect -> Q18）， Q18=（conflictRouteCheck -> Q19）， Q19=（noConflictRouteSetUp -> Q9）， Q20=（switchInCorect -> Q21|switchCorect -> Q23）Q21=（switchTransact -> Q22）， Q22=（switchTransactionErro -> Q3|switchCorrect -> Q23）Q23=（routeCheck -> Q24）， Q24=（routeEmpty -> Q25）， Q25=（conflictRouteCheck -> Q26）， Q26=（noConflictRouteSetUp -> Q9） Switch = Q0， Q0=（switchCheck -> Q1）， Q1=（switchInCorect -> Q2|switchCorect -> Q4）Q2=（switchTransact -> Q3）， Q3=（switchTransactionErro -> Q0|switchCorrect -> Q4）Q4=（switchLock -> Q5）， Q5=（switchLocked -> Q0） Section= Q0， Q0=（conflictRouteCheck->Q1|routeCheck -> Q4）， Q1=（conflictRouteExisting -> Q0 |noConflictRouteSetUp -> Q2）， Q2=（routeLock -> Q3）， Q3=（routeLocked -> Q0）， Q4=（routeOcupied -> Q0|routeEmpty -> Q5）， Q5=（conflictRouteCheck -> Q1） Signal = Q0， Q0=（signalClear -> Q1）， Q1=（signalCleared -> Q0） 在LTSA中执行组合运算后，得到系统的形式化模型如图2所示，与图2对应状态迁移关系的描述如下：
SysModel=Q0， Q0=（conflictRouteCheck->Q1|routeSelect->Q15）， Q1=（routeSelect->Q2）， Q2=（conflictRouteCheck -> Q3 |switchCheck -> Q10）， Q3=（conflictRouteExisting -> Q4 |noConflictRouteSetUp -> Q8）， Q4=（conflictRouteCheck -> Q5 |routeSetUpFailed -> Q7）， Q5=（routeSetUpFailed -> Q6）， Q6=（stop -> Q1）， Q7=（stop -> Q0 |conflictRouteCheck -> Q6）， Q8=（switchCheck -> Q9）， Q9= STOP， Q10=（switchInCorect -> Q11|switchCorect -> Q13）， Q11=（switchTransact -> Q12）， Q12=（switchTransactionErro->Q5 |switchCorrect -> Q13）， Q13=（switchLock -> Q14）， Q14= STOP， Q15=（conflictRouteCheck -> Q2 |conflictRouteCheck -> Q16|routeCheck -> Q17|switchCheck -> Q22）， Q16=（conflictRouteCheck -> Q3）， Q17=（routeOcupied -> Q4|routeEmpty -> Q18）， Q18=（conflictRouteCheck -> Q19|switchCheck -> Q21）， Q19=（switchCheck -> Q20）， Q20= STOP， Q21=（conflictRouteCheck -> Q20）， Q22=（conflictRouteCheck -> Q10|switchInCorect -> Q23|switchCorect-> Q25）， Q23=（conflictRouteCheck->Q11|switchTransact->Q24）， Q24=（switchTransactionErro -> Q4|conflictRouteCheck -> Q12|switchCorrect -> Q25）， Q25=（conflictRouteCheck -> Q13|switchLock -> Q26|routeCheck -> Q41）， Q26=（conflictRouteCheck -> Q14|routeCheck -> Q27）， Q27=（routeEmpty -> Q28）， Q28=（conflictRouteCheck->Q29|conflictRouteCheck->Q40）， Q29=（conflictRouteCheck->30）， Q30=（noConflictRouteSetUp->Q31）， Q31=（switchLocked-> Q32）， Q32=（routeLock -> Q33）， Q33=（routeLocked -> Q34）， Q34=（conflictRouteCheck -> Q35 |signalClear -> Q38）， Q35=（signalClear -> Q36）， Q36=（signalCleared ->Q37）， Q37=（routeSetUpOK->Q1）， Q38=（conflictRouteCheck->Q36|signalCleared->Q39）， Q39=（routeSetUpOK -> Q0|conflictRouteCheck -> Q37）， Q40=（conflictRouteCheck -> Q30）， Q41=（switchLock -> Q27|routeEmpty -> Q42）， Q42=（switchLock -> Q28|conflictRouteCheck -> Q43|conflictRouteCheck -> Q46）， Q43=（switchLock -> Q29|conflictRouteCheck -> Q44）， Q44=（switchLock -> Q30
耐2可知，各部件的形式化模型在模型检测工具LTSA中进行组合运算，没有出现错误标志“-1”，说明系统在进路建立过程中没有出现各部件单元因竞争资源而造成循环等待的死锁现象，系统功能正常。在LTSA中进行功能模拟显示，系统形式化模型能满足功能需求。
2系统安全性验证
通过对需求场景功能危害分析，得到系统进路基本安全需求模型如图3所示，其可判定条件集F={{ routeSelect， switchInCorect， routeSetUpOK}，{ routeSelect， switchLockFailure， routeSetUpOK}， {routeSelect， conflictRouteExisting， routeSetUpOK}， {routeSelect， sectionOccupied， routeSetUpOK}，{routeSelect， conflictSignalClear， routeSetUpOK}}，模型中迁移条件sectionOccupied表示区段占用，conflictSignalClear表示敌对信号开放，switchLockFailure表示道岔锁闭失效，其余迁移条件具体含义见表1。
图3表明系统发出进路预选命令后，不能在敌对进路建立、道岔不在规定位置、道岔锁闭失效、区段占用、敌对信号开放等情形下建立进路。 在LTSA中将图2所示系统形式化模型与图3所示模型作同步积运算，生成系统的同步积形式化模型，包含状态结点数为119，迁移数为210，应用前期研究成果“基于启发式on-the-fly的扩展TGBA模型检测算法”[13]，对系统同步积形式化模型进行安全性验证，检测结果为“No，空的ETGBA”，检测结点数为119，迁移数为210，所需时间为0.005 6秒，所需内存空间为8 872KB。由于安全性验证结果为“No”， 该系统的同步积形式化模型为空，表明系统在通常功能场景下的控制逻辑满足系统安全性要求，这一分析结果与当前铁路行业标准[14]中规定的基本联锁功能要求一致。 3结语
本文以铁路车站计算机联锁系统安全性分析为研究实例，首先对系统的进路建立子模块进行分析，建立半形式化描述的UML时序图；然后根据UML时序图进行形式化建模，用标号迁移系统模型对系统形式化建模进行描述；最后通过对需求场景功能危害进行分析，得出系统的基本安全属性，并用代数模型描述系统的基本安全属性，通过模型检测技术对系统进行安全性验证与分析，获得安全性分析结果。判空检测结果为空，证明本文建立的形式化模型是正确的，这一分析结果与当前铁路行业标准中规定的基本联锁功能要求相一致，验证了本文的一整套技术方法正确可行。 本文研究成果具有一定的理论价值和实践意义，可为安全苛求软件开发、安全性分析与验证、安全评估等提供有力的理论与技术支持，对于提高我国高速铁路、国防武器装备、航空航天等安全苛求领域的系统安全具有重要意义。
参考文献：
[1]赵志熙.计算机联锁系统技术[M].北京：中国铁道出版社，1999.
[2]S NEIL.Safety critical computer systems[M].Harlow，UK：AddisonWesley Longman.1996.
[3]郦萌，吴芳美.铁路信号可靠性安全性理论及证实[M].北京：中国铁道出版社，2008.
[4]张越，王海峰.基于Event-B的计算机联锁安全规范描述与验证[J].计算机与通信信号，2013，12（11）：4749.
[5]陶玲， 宋军.基于CPN的联锁进路控制建模及验证[J].工业控制计算机，2014， 27（11）： 1216.
[6]王曦，徐中伟.基于场景分析的系统形式化模型生成方法[J].计算机科学，2012， 39（8）： 136140.
[7]Y M HON， M KOLLMANN.Simulation and verification of UMLbased railway interlocking designs[J].AvoCS，2006（6）：168172.
[8]K NAKAMATSU，Y KIUCHI，W Y CHEN，et al.Intelligent railway interlocking safety verification based on annotated logic program and its simulator[C].In： Proceedings of 2004 IEEE International Conference on Networking， Sensing and Control，Taipei， Taiwan： 2004： 694699.
[9]ABRIAL J R.Modeling in eventB：system and software engineering [M].Cambridge University Press，Cambridge，2010.
[10]P BEHM，M T OR.A successful application of B in a Large project[J].FM’99Formal Methods，1999（6）：712722.
[11]熊振A，魏臻.基于UPPAAL的铁路车站信号联锁系统模型验证[J].科学技术与工程，2008，8（7）：18431846.
[12]燕飞，唐涛.计算机联锁控制逻辑的模型检验方法[J].铁道通信信号，2009，45（5）：2629.
[13]王曦，徐中伟.基于启发式onthefly的扩展TGBA模型检测算法[J].计算机学报， 2014，37（12）：25192529.
[14]中华人民共和国铁道部.TB/T 30272002计算机联锁技术条件[M].北京： 中国铁道出版社， 2002.
