基于时间自动机的列控中心软件形式化建模与验证

摘要

列车运行控制系统是我国高速铁路的核心技术之一，目前我国高速铁路均采用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软件的逻辑性、时序性和故障-安全性。

目录

声明

致谢

摘要

1 引言

1．1 选题背景和意义

1．2 国内外研究现状

1．2．1 国外研究现状

1．2．2 国内研究现状

1．3 CTCS-3级列车运行控制系统仿真测试平台介绍

1．4 论文主要工作

2 时间自动机理论和UPPAAL介绍

2．1 形式化方法概述

2．2 时间自动机理论

2．2．1 时间自动机概述

2．2．2 可达性分析

2．3 模型分析工具UPPAAL

2．3．1 UPPAAL特征和结构

2．3．2 UPPAAL的系统描述语言

2．4 本章小结

3 报文编制流程的分层形式化建模

3．1 TCC分层方案的设计

3．2 报文编制流程的分层设计

3．2．1 相关接口分析

3．2．2 报文编制的场景分类

3．2．3 报文编制的功能层设计

3．2．4 报文编制的计算实现

3．3 报文编制流程分层模型的建立

3．3．1 接口层模型

3．3．2 场景层模型

3．3．3 功能层模型

3．3．4 计算层模型

3．4 报文编制流程的时间自动机网络的构建

3．5 本章小结

4 基于UML与AT的轨道电路编码流程的建模

4．1 基于UML与AT建模的特点

4．2 轨道电路编码流程的UML类图的建立

4．3 轨道电路编码流程的UML状态图的建立

4．3．1 TS信息处理

4．3．2 CI信息处理

4．3．3 编码模块

4．3．4 轨道电路编码主逻辑控制模块

4．4 时间自动机的建模

4．4．1 TS信息处理

4．4．2 CI信息处理

4．4．3 编码模块

4．4．4 轨道电路编码主逻辑控制模块

4．5 本章小结

5 模型的仿真及验证

5．1 UPPAAL模拟仿真

5．2 UPPAAL验证及错误处理

5．2．1 功能验证

5．2．2 软件错误推断检测

5．3 TCC软件实现及验证

5．4 本章小结

6 结论与展望

6．1 结论

6．2 展望

参考文献

图索引

表索引

作者简历

学位论文数据集