列控系统TSRS形式化建模分析与验证

摘要

临时限速是指除线路规定的限速以外，由于施工、维修等原因引起的有计划的限速和由于自然灾害、设备故障等原因引起的突发限速。临时限速的设置关乎到提高运输效率和保障行车安全，随着列车速度的越来越快，对临时限速设置的安全性要求也越来越高。临时限速系统是列控系统的重要组成部分，是涉及到行车安全和运输效率的安全苛求系统。临时限速的工作流程具有严格的时序逻辑关系，体现出精确的时间约束特性。
　　针对临时限速系统的这些特性，有必要对其工作流程的实时性进行分析，采用形式化方法对系统的特性和行为进行建模描述，验证所产生的结果在逻辑和时间上的正确性及系统的实时性，从而发现系统规范的不完备性和模糊性，保证系统的安全性，为完善设计和开发提供重要的依据。
　　本文通过分析临时限速系统的结构，理清各设备之间的信息交互关系，结合临时限速系统的功能及调度命令的操作流程，说明各信息的交互方式;利用时间自动机理论对临时限速系统进行建模，并结合高铁CTC调度台分界口、CTCS等级转换区这两个特殊场景不同的工作流程建立各自的时间自动机模型。通过模型对系统的行为进行了精确的描述，避免了规范的不完备性和模糊性。提取临时限速系统的功能属性和性能属性要求并给出其BNF语法描述。在时间自动机模型的基础上，利用UPPAAL工具对模型进行时序逻辑的仿真，得到系统工作流程的仿真时序图，利用验证器对各模型的功能和性能属性进行验证。验证结果说明了系统的时间特性、受限活性和安全性。

目录

声明

摘要

第1章 绪论

1．1 研究背景及意义

1．2 研究现状

1．2．1 形式化方法在列控领域的研究现状

1．2．2 时间自动机在列控领域的研究现状

1．3 本文研究的主要内容

第2章 临时限速系统分析

2．1 临时限速系统结构

2．2 临时限速系统信息交互接口

2．3 临时限速操作流程

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

2．3．2 临时限速命令的设置

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

2．4 小结

第3章 临时限速系统形式化建模

3．1 时间自动机理论

3．2 临时限速系统时间自动机网络分析

3．3 临时限速数据流时间自动机建模方法

3．4 临时限速系统时间自动机模型的建立

3．4．1 CTC时间自动机模型

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

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

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

3．4．5 临时限速系统时间自动机网络

3．5 小结

第4章 特殊场景限速方案建模

4．1 高铁CTC调度台交界口临时限速

4．1．1 调度台分界口限速流程模型

4．2 CTCS等级转换区临时限速

4．2．1 CTCS等级转换区限速流程模型

4．3 小结

第5章 模型的仿真与验证

5．1 仿真验证工具UPPAAL

5．2 临时限速系统模型的仿真与验证

5．3 特殊场景限速方案模型仿真与验证

5．3．1 高铁CTC调度台交界口临时限速模型仿真与验证

5．3．2 CTCS等级转换区临时限速模型仿真与验证

5．4 系统模型仿真界面

5．5 小结

结论

致谢

参考文献

攻读硕士学位期间发表的论文及科研成果