车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真

摘要：在铁路联锁系统中，联锁软件是一个至关重要的组成部分，提高联锁软件的质量和可靠性是十分重要的。本文介绍了联锁软件的基本结构和原理，分析了联锁的进路控制流程，并采用时间自动机UPPAAL软件，分别针对联锁进路的建立、道岔控制、信号开放和保持、解锁及消息处理的功能模块进行了设计。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 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真:http://www.youerw.com/shuxue/lunwen_767.html