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