论文部分内容阅读
CTCS-3级列车运行控制系统是我国目前应用等级最高、技术设备最先进的铁路信号设备,主要用于保证列车安全、高效地运行。列车自动防护系统(Automatic Train Protection,ATP)是CTCS-3级列车运行控制系统的核心部分,其是一个典型的安全关键系统,其系统功能复杂,失效后可能导致发生重大安全事故,造成重大人员伤亡和财产损失。因此,ATP的安全性和可靠性直接关系着列车的运行安全。形式化建模是安全关键系统开发的重要方法之一。高安全性应用开发环境(Safety Critical Application Development Environment,SCADE)提供的“基于模型”的形式化建模方法,具有严格的数学理论基础,能实现对系统需求的准确、无歧义表达,能够有效地解决传统软件开发方法中存在的模糊性和二义性问题,并能够实现需求的逻辑推理。运用SCADE建立形式化模型能够清晰、准确地表达系统的功能逻辑;结合SCADE的模型仿真和形式化验证能够全面地分析模型的正确性和安全性,避免开发人员的主观性。本文研究基于SCADE的ATP开发方法,利用SCADE需求管理工具管理和分析了需求,采用形式化建模方法建立了ATP模型,并使用SCADE仿真器和形式化验证方法来验证SCADE形式化模型,保证了ATP的安全性和正确性,具体包括以下几个方面:(1)介绍了SCADE的需求管理方法及其应用优势,详细分析了SCADE的形式化建模、模型仿真方法和形式化验证。(2)简述了CTCS-3级列车运行控制系统地面设备和车载设备的主要组成及功能,介绍了ATP的基本原理及主要功能,并主要分析了速度控制、模式转换和等级转换功等关键功能。(3)根据系统需求将关键功能细分为TSM和CSM区的速度控制、模式转换、CTCS-2到CTCS-3和CTCS-3到CTCS-2的等级转换,分析各关键功能的具体处理逻辑,并采用SCADE形式化建模方法建立各功能的形式化模型。(4)利用SCADE需求管理工具分析ATP系统需求、概要设计和形式化模型之间的追溯关系;通过SCADE仿真器对模型进行仿真,检查ATP模型的正确性;然后提取系统安全属性,利用SCADE的形式化验证器对模型进行形式化验证,证明模型满足预期安全需求,保证了模型的安全性和正确性。