基于模型检测的区间占用逻辑检查形式化建模与验证

摘要

轨道电路作为铁路信号系统基础设备，主要用于反映区间闭塞分区占用情况，其可靠性与安全性对于铁路运输安全起着至关重要的作用。当轨道电路发生分路不良或故障占用时，轨道继电器状态发生错误变化，此时无法准确判断列车占压区间情况，从而出现“红光带”、“丢车”等现象，引起安全隐患。区间占用逻辑检查则是现阶段针对上述轨道电路故障而采取的解决方法，它借鉴站内联锁“三点检查”原理，加入时序约束，根据区间列车运行方向以及占用出清闭塞分区的顺序，进行相应的逻辑计算，预处理不可信轨道继电器状态变化信息，有效降低行车风险，因此对区间占用逻辑检查进行分析研究具有重要意义。　　由于区间占用逻辑检查原理复杂，且检查过程有实时性要求，传统的仿真测试方法不能及时发现逻辑制定过程中出现的人为分析错误，所以本文采用形式化方法对区间占用逻辑检查进行分析验证，以期提高其逻辑正确性，保证安全性。通过分析区间占用逻辑检查功能特点，对比目前铁路领域常用形式化建模验证方法优缺点，选用时间自动机理论作为研究方法，UPPAAL作为验证工具。　　本文以软件式区间占用逻辑检查为研究对象，以逻辑检查原理为研究目标，阐述了区间占用逻辑检查实现过程。为降低复杂度，根据区间占用逻辑检查的功能特点及作用范围将其分为本站占用逻辑检查和两站逻辑检查信息交互两个子过程，分别对两个子过程的实现流程以及功能作用具体场景进行分析，确定各子过程中包含对象，提取各对象行为动作，用形式化语言描述，构建各对象时间自动机模型，同时为增加模型完整性，尽可能模拟区间行车真实状态，在本站占用逻辑检查模型中注入闭塞分区故障模型，在两站逻辑检查信息交互模型中注入通信故障模型，组成对应时间自动机积，再利用UPPAAL验证其功能性和实时性，导出安全应用场景。　　基于以上模型分析验证基础，编程实现了仿真系统的设计开发，并对其功能进行测试。测试结果与预期结果一致，表明了区间占用逻辑检查模型的正确性，进一步验证了区间占用逻辑检查的安全性和可行性。

目录

声明

第1 章绪论

1.1 研究背景及意义

1.2 国内外研究现状

1.2.1 区间占用逻辑检查研究现状

1.2.2 形式化方法在铁路领域中的应用现状

1.3 论文内容和结构安排

第2 章区间占用逻辑检查特点分析及形式化方法研究

2.1 区间占用逻辑检查特点

2.2 形式化方法研究

2.3 形式化方法选择

2.4 时间自动机及UPPAAL

2.4.1 时间自动机研究

2.4.2 验证工具UPPAAL

2.5 本章小节

第3 章区间占用逻辑检查分析

3.1 区间占用逻辑检查工作流程分析

3.1.1 整体实现流程划分

3.1.2 闭塞分区逻辑检查原理

3.2 本站占用逻辑检查分析

3.2.1 本站占用逻辑检查实现流程

3.2.2 本站区间信号许可处理分析

3.3 两站逻辑检查信息交互分析

3.3.1 两站逻辑检查信息交互实现流程

3.3.2 信号许可信息交互分析

3.4 本章小结

第4 章 区间占用逻辑检查的建模与验证

4.1 本站占用逻辑检查的时间自动机模型

4.1.1 本站占用逻辑检查规范性描述

4.1.2 本站占用逻辑检查模型的建立

4.2 两站逻辑检查信息交互时间自动机模型

4.2.1 两站逻辑检查信息交互规范性描述

4.2.2 两站逻辑检查信息交互模型的建立

4.3 模型的仿真及验证

4.3.1 本站占用逻辑检查模型的仿真及验证

4.3.2 两站逻辑检查信息交互模型的仿真及验证

4.4本章小结

第5章区间占用逻辑检查仿真系统的设计与实现

5.1 系统总体设计

5.1.1 仿真系统目标

5.1.2 系统架构设计

5.2 系统模块的设计与实现

5.2.1 初始化闭塞分区处理模块

5.2.2 运行闭塞分区逻辑处理模块

5.2.3 信号许可模块

5.2.4 信息交互模块

5.2.5 报警模块

5.2.6 人机交互模块

5.3 功能测试

5.4 本章小结

结论与展望

致 谢

参考文献

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