论文部分内容阅读
在城市轨道交通信号系统中,联锁系统是保证行车安全的重要设备,同样也是安全关键系统,必须满足安全完整性等级SIL-4级安全需求,它直接关系到人民的生命和财产安全。利用传统的开发方法设计并开发联锁系统,难度高且不易寻找错误和安全隐患,基于模型的软件开发方法在安全关键领域逐渐被接受。高安全性应用开发环境(Safety Critical Application Development Environment,SCADE),为高安全性系统的软件开发提供了一套基于模型的嵌入式软件开发的方案,可以减少软件开发风险,缩短验证时间,降低开发成本。但安全属性的难以表达以及安全模型的庞大,给验证和安全分析工作带来困难。本文基于SCADE对移动闭塞下的联锁功能模型进行搭建,为保证系统安全性,提出基于故障树分析(FaultTree Analysis,FTA)的SCADE联锁功能模型安全性分析与验证方法。论文主要工作有:(1)分析城轨联锁系统结构与功能需求,研究移动闭塞下特殊进路以及对进路控制过程的要求。实现联锁功能模块概要设计,根据进路状态,将进路控制功能模块划分为选路模块、选排一致检查模块、进路检查模块、信号开放模块、接近锁闭模块、正常解锁模块以及取消进路模块;(2)基于SCADE对联锁功能模块进行设计并建模,完成了移动闭塞下进路控制功能模块的建模,在正线进路控制的基础上,实现了对多列车进路、折返进路、自动进路以及保护进路的控制;(3)结合SCADE形式化验证过程,提出了基于故障树的SCADE联锁功能模型安全分析与验证方法,搭建了 SCADE环境下联锁模型的验证框架。基于FTA分析联锁功能模型的安全性,构建功能模型的故障树模型,将其作为安全特性模型进行形式化验证;(4)提出基于失效模式与影响分析(Failure Modes and Effect Analysis,FMEA)搭建联锁功能模型故障树的方法,构建了进路控制功能模块的故障树;以进路建立过程为例,搭建故障树模型,分析进路建立功能模型的安全性,并通过故障注入,证明了功能模型故障树作为安全特性模型的有效性。基于SCADE设计开发联锁系统,有助于减少联锁软件设计和开发过程中的不安全隐患和潜在错误,进而提高联锁软件的可靠性和安全性。结合FTA分析联锁功能模型的安全性,并进行形式化验证,体现出形式化验证的完备性,更为全面的分析了模型的安全性,避免了形式化验证过程中安全属性难以表达及安全特性模型庞大的问题。