基于UPPAAL的ETCS-1级/ETCS-NTC级等级转换形式化建模

发布时间：2021-03-07 18:00

　　与航空、公路等交通方式相比,铁路运输具有运量大、环境友好、准点率高等优点,使得铁路运输在各国交通运输体系中占有重要的地位。列车运行控制系统是铁路信号的重要组成部分,是保障行车安全、提高运输效率和行车速度的关键子系统。随着我国"一带一路"的战略的实施,如何满足互联互通需求和安全技术保障成为了铁路信号领域所关注的问题。ETCS是为实现互联互通而制定的列控技术规范,其中ETCS-1级与ETCS-NTC级之间的等级转换是欧洲列控系统和本国列控系统之间的转换,因此对两者之间等级转换的研究非常有必要。通过形式化模型对系统进行设计和验证,可以保证系统设计开发的正确性和安全性。本文在对ETCS系统需求规范、专用传输模块接口规范、互联互通性能要求规范进行需求分析的基础上,建立了 ETCS-1/ETCS-NTC等级转换的列控车载设备、轨旁单元和系统环境间信息交互的时间自动机模型,最后对模型进行仿真和形式化验证。首先,从系统功能架构和系统应用等级方面对ETCS进行了介绍,阐述了 ETCS的适用范围、系统组成、系统环境和应用现状。其次,对列控车载设备从开始任务进入ETCS-1级、到与专用传输模块连接,ETCS... 

【文章来源】：西南交通大学四川省 211工程院校 教育部直属院校

【文章页数】：70 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第1章 绪论
    1.1 研究背景和意义
    1.2 国内外研究现状
        1.2.1 国内现状
        1.2.2 国外现状
    1.3 论文的主要工作
第2章 系统建模和形式化方法
    2.1 系统建模与验证
        2.1.1 建模方法
        2.1.2 验证方法
    2.2 基于时间自动机的建模
        2.2.1 状态转移系统
        2.2.2 时间自动机的语义和语法:
        2.2.3 时间自动机网络
    2.3 模型验证工具UPPAAL
        2.3.1 UPPAAL的结构和特征
        2.3.2 UPPAAL的描述语言
    2.4 本章小结
第3章 ETCS-1/ETCS-NTC等级转换建模
    3.1 ETCS列控系统概述
        3.1.1 系统结构
        3.1.2 应用等级
    3.2 列车进入ETCS-1级与STM连接
        3.2.1 开始任务场景分析
        3.2.2 开始任务进入ETCS-1级模型
        3.2.3 STM与ETCS连接场景分析
        3.2.4 STM与ETCS连接模型
    3.3 ETCS-1向ETCS-NTC转换
        3.3.1 场景分析
        3.3.2 ETCS-1向ETCS-NTC转换模型
    3.4 ETCS-NTC向ETCS-1转换
        3.4.1 场景分析
        3.4.2 ETCS-NTC向ETCS-1转换模型
    3.5 本章小结
第4章 模型的验证分析
    4.1 仿真验证
    4.2 形式化验证
        4.2.1 功能需求的验证
        4.2.2 安全性的验证
        4.2.3 时间约束的验证
    4.3 本章小结
总结
致谢
参考文献



本文编号：3069558