论文部分内容阅读
摘要：列车运行控制系统是我国高速铁路的核心技术之一,目前我国高速铁路均采用CTCS-3级列控系统作为统一技术平台。CTCS-3级列控系统是一个安全性要求极高的系统,对其进行功能及性能的安全性验证和评估非常重要。采用计算机技术,在实验室搭建CTCS-3级列控系统仿真平台对其进行辅助研究和预研验证具有实际意义。列控中心(TCC)是CTCS的关键设备之一。在CTCS-2级列控系统的地面设备中,TCC作为核心安全设备,产生控车信息控制列车运行,是保证列车安全运行的关键信号设备。作为CTCS-3后备系统,TCC是不可缺少的重要组成设备,其可靠性和实时性影响到整个高速铁路的安全高效运行,保证TCC软件的可靠性和实时性显得尤为重要。为了在CTCS-3级列控系统仿真平台中开发安全可靠的TCC软件,本文结合时间自动机理论,对TCC软件进行形式化语义描述,使用基于时间自动机理论的建模验证工具对TCC软件进行建模,并验证分析软件特性,从而保证在软件设计逻辑下,TCC可以高效准确地生成控车信息。论文提出两种适合于TCC软件的建模方法,分别是基于时间自动机的分层建模方法和采用UML与时间自动机相结合的建模方法。针对分层建模方法,以有源应答器报文编制流程为例：首先根据流程的特点,对有源应答器报文编制功能进行分层设计；其次,经过合理的抽象和假设,对分层设计建立成员时间自动机；再次,通过设置通道和全局变量,在模型验证工具中建立时间自动机网络；最后,在工具中模拟验证模型的功能和性能。针对UML与时间自动机相结合的建模方法,以TCC的轨道电路编码功能为例：首先进行软件设计的分类整理,根据软件概要设计建立UML类图；再针对软件详细设计流程,建立UML状态图；最后根据UML与时间自动机对应规则,将UML模型转换为时间自动机模型,并在模型验证工具中对其进行模拟验证。通过以上验证,对模型检验结果与需求存在不一致的方面及时纠正设计流程,并再次检验。通过反复修改检验,最终得出实时高效的设计流程,根据流程对TCC软件进行编程实现,进而确保TCC软件的逻辑性、时序性和故障-安全性。