论文部分内容阅读
测速定位系统是城市轨道交通列车运行控制系统车载设备的关键子系统,它实时检测列车速度与当前位置,所测数据将用于列车移动授权的计算,测速定位系统的精确性和可靠性直接影响着行车安全和效率。基于模型的软件开发方法如今在安全关键领域逐渐被认可,高安全性应用开发环境(Safety critical application development environment, SCADE),为安全苛求系统、软件研发人员提供认证级解决方案,其基于模型的开发方式、内置仿真器与模型验证工具Design Verifier保证了所开发系统的功能性及安全性。本文基于SCADE对测速定位系统进行建模、仿真、验证及安全性分析。本文主要工作有：1、以地铁列车运行控制系统为背景,研究了安全关键性系统的开发方式,分析了基于模型开发方式的优点,详细介绍了SCADE高安全性应用开发环境。2、根据地铁列车测速定位系统的功能特点,将测速定位系统划分为轮径校正、列车位置初始化、列车位置确定和列车定位失效管理4个子系统,并详细分析了这些子系统的流程,设计了各个子系统的建模方法。3、为了提高列车测速定位系统设计的安全性,依据轨道交通1474.3规范,基于形式化模型驱动开发理论,使用高安全性应用开发环境(SCADE)的数据流图和安全状态机建模机制对测速定位系统的各个子系统建立模型,通过各子系统接口整合各子系统模型,最终得到完整的测速定位系统模型。4、依据模型内置的逻辑运算公式和模型运行中产生的中间数据,使用SCADE的仿真与验证工具,通过验证逻辑运算结果,达到检验模型功能和安全性的目的。通过验证证明所设计模型满足系统功能性和安全性需求。5、在使用SCADE验证了模型整体安全性的基础上,基于Deductive Cause-Consequence Analysis (DCCA)方法严厉的逻辑框架,分析了导致测速定位系统危害的失效模式,使用SCADE验证机制寻找出了导致测速定位系统危害的最小关键集,为高安全性系统的设计提供依据。6、利用SCADE KCG代码生成器通过了轨道交通EN 50128SIL 3/4级认证以及SCADE能从需求规范自动生成嵌入式源代码特点的优势,使用KCG自动生成测速定位系统高质量高安全C语言代码,使系统可直接应用到工程产品中。