基于时间自动机的高铁列控系统TSRS的建模分析与验证

摘要

临时限速系统是高铁列控系统的核心构成之一，临时限速系统的工作流程严格依照客运专线列控系统临时限速技术规范来实现。技术规范中规定临时限速分为计划性限速和突发性限速，其两者都具有严格的时间逻辑关系和时间约束特性。技术规范的制定和执行都存在一定的人为因素干扰，为了保证铁路系统运营的安全和效率需要对技术规范进行合理的优化管理。　　临时限速系统作为高铁列控系统安全保障的核心环节，其安全性和受限活性受到运营场景的限制。因此运用形式化的分析方法对系统流程、发生事件和逻辑时间关系进行形式化分析和建模描述，验证系统在逻辑上的安全性和时间变化上的受限活性满足高铁列控系统的正确性要求。从而发现形式化描述的临时限速系统存在定义上的二义性和不可达性，找出系统中存在的缺陷为后续临时限速系统的优化和深层次的开发提供重要的理论验证依据。　　本文通过分析临时限速命令拟定校验、下达和执行反馈等基本操作流程，同时结合信息之间的交互关系和交互方式，并利用时间自动机理论可以建立三部分的时间自动机网络模型:非跨界临时限速时间自动机模型、跨界临时限速时间自动机模型和TSRS(Temporary Speed Restriction Server，临时限速服务器)切换与RBC(Radio BlockCenter，无线闭塞中心)切换重叠区域临时限速交互流程的时间自动机模型。这三个不同特殊场景下的时间自动机网络模型描述了系统临时限速命令的交互流程，根据系统要求的实时性和可达性设置不同的时间参数。根据上述时间自动机模型的规范描述和技术规范的要求，应用形式化BNF(Backus Normal Form，巴科斯范式)语法描述不同场景下时间自动机模型的验证语句，并将BNF验证语句输入到验证工具UPPAAL中对系统的安全性和受限活性进行验证，同时找出不满足临时限速系统受限活性要求的BNF语句对其中涉及到的时间约束变量进行分析，并给出解决方案。验证结果表明:根据系统建立的时间自动机模型满足其安全性要求，同时其受限活性中的时间参数变量指出临时限速技术规范中的不足。

目录

声明

摘要

1 绪论

1．1 论文的选题背景和研究意义

1．2 国内外研究现状

1．2．1 国内研究现状

1．2．2 国外研究现状

1．2．3 研究现状分析

1．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 临时限速系统的构成

3．2 临时限速命令的操作流程

3．2．1 临时限速命令的拟定

3．2．2 临时限速命令的下达

3．2．3 临时限速命令的取消

3．3 小结

4 高铁列控非跨界临时限速系统的形式化建模

4．1 临时限速系统的安全性和受限活性要求

4．2 非跨界临时限速系统时间自动机模型的建立

4．2．1 TSRS时间自动机模型

4．2．2 CTC时间自动机模型

4．2．3 TCC时间自动机模型

4．2．4 RBC时间自动机模型

4．3 非跨界临时限速系统时间自动机网络

4．4 小结

5 高铁列控系统中特殊场景的形式化建模

5．1 跨界临时限速系统的分析

5．1．1 跨界临时限速命令的拟定

5．1．2 跨界临时限速命令的执行下达

5．1．3 跨界I临时限速命令的取消和删除

5．1．4 跨界临时限速命令的同步

5．2 跨界临时限速系统的建模

5．2．1 跨界临时限速系统时间自动机模型

5．2．2 跨界临时限速系统时间自动机网络

5．3 TSRS切换和RBC切换重叠区域限速流程的建模

5．3．1 TSRS切换和RBC切换重叠区域时间自动机模型的建立

5．3．2 TSRS切换和RBO切换重叠区域时间自动机网络

5．4 小结

6 基于UPPAAL的模型验证分析

6．1 非跨界临时限速模型的验证分析

6．2 跨界临时限速模型的验证分析

6．3 TSRS切换和RBC切换重叠区域限速流程模型的验证分析

6．4 小结

结论

致谢

参考文献

攻读学位期间的研究成果