列车自动防护系统的形式化建模与验证

摘要

列车自动防护(ATP)系统是列车运行控制系统的核心子系统，系统的安全性和可靠性直接关系到列车的运行安全。ATP系统作为典型的、复杂的安全苛求实时系统，系统功能复杂，系统内部相互通信频繁，对实时性有很高的要求。系统既要求逻辑运算结果是正确的，又要求必须在规定的时间限制内产生结果。如何保证开发的ATP系统功能与系统需求规范的一致性，进而保证系统的正确性和安全性成为研究人员亟待解决的问题。
　　形式化方法是以严格的数学理论为基础，可以对系统需求规范进行准确的描述，避免了自然语言的随意性，能够很好地解决上述问题。本文在对形式化方法进行分析和比较的基础上，选择时间自动机理论描述实时并发系统功能流程。以ATP系统为例对时间自动机进行详细的分析，研究了构建系统时间自动机网络模型的方法，并对UPPAAL这种行为模型验证工具进行了详细的研究。
　　论文以轨道交通列车自动防护系统为研究对象，对系统的功能进行详细的分析，着重研究了系统的速度监督与超速防护功能以及同步功能。针对系统功能需求，采用UPPAAL模型验证工具对超速防护和同步功能流程进行形式化建模，并对模型的安全性和受限活性进行验证。通过验证，证明了模型功能与系统需求的一致性，表明使用时间自动机对ATP系统流程进行建模和分析，是保障ATP系统功能正确性和安全性非常重要的途径。论文用VC6.0软件工具对车载ATP速度防护模型进行了设计与仿真，实现了车载ATP的速度监督与超速防护功能。

目录

声明

摘要

第1章 绪论

1．1 列车运行控制技术的研究背景

1．2 列车运行控制系统的形式化研究现状

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

1．4 本文组织结构

第2章 ATP系统组成及功能分析

2．1 系统组成

2．1．1 地面ATP系统

2．1．2 车载ATP系统

2．2 车载ATP系统功能分析

2．2．1 速度监督与超速防护流程

2．2．2 同步流程分析

2．3 ATP系统安全性需求

2．4 本章小结

第3章 ATP功能流程的形式化建模

3．1 ATP系统与形式化方法

3．1．1 时间自动机的分析

3．1．2 验证工具的分析

3．2 速度监督与超速防护流程模型

3．3 同步流程模型

3．4 本章小结

第4章 ATP功能模型的形式化仿真与验证

4．1 模型仿真时序图分析

4．1．1 TA模型状态转移过程模拟

4．1．2 CF模型状态转移过程模拟

4．2 模型属性验证

4．2．1 TA模型验证

4．2．2 CF模型验证

4．3 本章小结

第5章 车载ATP速度防护模型设计

5．1 车载ATP速度防护曲线模型研究

5．2 速度防护曲线的计算模型设计

5．3 系统速度防护功能的仿真设计

5．3．1 车载ATP系统工作流程设计

5．3．2 车载ATP系统速度防护功能的仿真

5．4 本章小结

结论

致谢

参考文献

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