车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真
关键词： UPPAAL；车站联锁；计算机联锁；时间自动机4213
Railway Interlocking System and UPPAAL Modeling
Abstract：In the Railway interlocking system, interlocking software is the key component. Enhancing the quality and the reliability of the interlocking software is very important for designing the computer interlocking system. The paper presents the base structure and theory of the interlocking software. The UPPAAL software is applied to simulate different function models of interlocking system, including the route establishment, switch controlling, the signal opening and holding, the route unlocking and message processing. The UPPAAL network model based on systematic timed automata theory uses graph language to describe logic behaviors of the system, and describes the real-time performance by adding the time constraints. This model can avoid inconsistencies, ambiguities and incompleteness of the interlocking system. Finally, the model is simulated and verified.. The results show that using timed automata model can effectively reduce the fault in system design, and promote the system reliability of interlocking software.
Key Words： UPPAAL；railway interlocking；computer interlocking；timed automata
目录
1 绪论 1
1.1 中国铁路的发展背景和现状 1
1.1.1 中国铁路的发展背景 1
1.1.2 中国铁路发展现状 1
1.2 计算机联锁概述 2
1.2.1 计算机联锁的发展 2
1.2.2 车站联锁系统的基本结构 3
1.2.3 计算机联锁的特点 4
1.3 选题的目的和意义 5
2 时间自动机理论和UPPAAL介绍 6
2.1 形式化方法概述 6
2.1.1 形式化规范 6
2.1.2 形式化验证 6
2.2 时间自动机理论 7
2.3 模型分析验证工具UPPAAL介绍 7
2.3.1 UPPAAL的结构和特征 7
2.3.2 UPPAAL的系统描述语言 9
3 基于时间自动机的联锁进路控制流程分析 11
3.1 联锁软件设计开发的框架 11
3.2 联锁软件的结构 12
3.3 联锁软件的需求分析 13
3.3.1 功能需求 13
3.3.2 性能需求 13
3.4 联锁进路控制流程分析与设计 14
4 联锁进路建模及仿真 16
4.1 进路选排 16
4.1.1 进路选排流程分析 16
4.1.2 进路选排模型 17
4.1.3 进路选排模拟仿真 21
下一篇：投资者情绪与股票收益率的关系研究