CTCS-1级列控系统RDC数据生成及验证方法的研究
发布时间：2021-05-10 06:49
中国列车运行控制系统（Chinese20Train20Control20System,CTCS）是保障列车运行安全和效率的安全苛求系统。列控数据作为信号设备信息、列车状态信息和线路信息的载体,其正确性是列车安全运行的重要前提。目前针对不同的列控子系统,数据描述方式不同且没有特定的数据规范,列控数据的验证也主要依靠人工校验和仿真测试相结合的方式,效率低且正确性难以保证。针对上述问题,本文以研究CTCS-1级列控系统地面核心设备—区域列控数据中心（RDC）的静态数据验证为例,从RDC数据组织方式设计和数据验证两个方面进行了研究,首先建立了20RDC静态数据模型,然后提出了数据验证的总体框架,设计和开发了20RDC数据自动化验证工具,实现了数据的自动化验证。论文完成的工作包括:（1）设计RDC数据组织方式,建立RDC静态数据模型。通过分析RDC系统需求将数据分为点元素、线元素和区域元素,构建各数据元素之间的逻辑关系模型,使之既体现线路拓扑关系又便于后期维护和更新,最终建立RDC静态数据结构模型,并结合实际线路数据生成RDC静态数据库。（2）提出数据建模和验证的总体框架,将其分为四个阶段:数据...
【文章来源】：北京交通大学北京市 211工程院校 教育部直属院校
【文章页数】：111 页
【学位级别】：硕士
【文章目录】：
致谢
摘要
ABSTRACT
1 引言
1.1 研究背景和意义
1.1.1 研究背景
1.1.2 选题目的及意义
1.2 数据验证研究现状
1.2.1 列控系统数据验证研究现状
1.2.2 其他领域数据验证研究现状
1.3 CTCS-1级列控系统概述
1.4 论文的研究内容和框架
2 数据验证的理论基础
2.1 数据设计模型概述
2.2 通信顺序进程形式化建模方法
2.2.1 CSP方法概述
2.2.2 通信顺序进程CSP语义和语法
2.3 CSP模型-Petri网模型转换方法
2.3.1 Petri网基本概念
2.3.2 CSP-Petri网模型转换规则
2.4 本章小结
3 RDC静态数据生成
3.1 RDC概述
3.2 RDC静态数据需求分析
3.3 RDC数据组织方式分析
3.4 RDC静态数据模型建立
3.5 RDC静态数据生成实例
3.6 本章小结
4 RDC数据验证CSP模型的建立
4.1 RDC数据验证总体框架
4.2 RDC数据建模验证的总体思路
4.3 数据约束规则提取和验证方法设计
4.3.1 数据约束规则提取
4.3.2 约束规则管理
4.3.3 数据验证方法设计
4.4 数据验证CSP模型
4.4.1 数据验证总体模型
4.4.2 验证轨道区段数据CSP模型
4.4.3 验证进路数据CSP模型
4.5 本章小结
5 数据验证模型的形式化验证
5.1 模型检验方法
5.2 验证工具ProB
5.2.1 ProB概述
5.2.2 CSP_M语言转换
5.3 CSP语义模型检验
5.3.1 性质验证分析
5.3.2 数据验证模型正确性检验
5.3.3 数据验证模型功能性检验
5.3.4 数据验证模型安全性检验
5.3.5 验证结果分析
5.4 本章小结
6 RDC数据自动化验证工具的设计与实现
6.1 需求分析
6.2 软件设计
6.2.1 软件总体设计
6.2.2 数据审核逻辑模块详细设计
6.3 软件实现
6.3.1 开发环境
6.3.2 软件主界面
6.4 实际线路数据验证
6.5 本章小结
7 结论
7.1 总结
7.2 展望
参考文献
图索引
表索引
作者简历及攻读硕士学位期间取得的研究成果
学位论文数据集
【参考文献】：
期刊论文
[1]高速铁路产业发展的区域布局研究——基于中国铁路中长期发展规划政策[J]. 闫昱霖. 经济师. 2017(11)
[2]列车运行控制数据校核及管理系统[J]. 吕瑞,马春英. 铁道通信信号. 2017(02)
[3]基于SAT的应答器工程数据逻辑规则提取及验证[J]. 王彤典,赵会兵. 铁道学报. 2017(02)
[4]CTCS-1级列控系统总体技术方案探讨[J]. 莫志松. 中国铁路. 2016(08)
[5]城轨计算机联锁的数据安全性验证[J]. 周果,赵会兵. 铁道学报. 2016(08)
[6]列控工程数据自动审核的研究与实现[J]. 陈倩佳,卢佩玲. 铁路计算机应用. 2015(03)
[7]CTCS-0列控系统改造方案研究[J]. 黄玉祥. 中国铁路. 2014(09)
[8]基于进程迹的CSP模型验证框架[J]. 赵岭忠,翟仲毅,钱俊彦. 计算机科学. 2013(11)
[9]列控数据完备性建模方法研究[J]. 程忆佳,王俊峰. 铁路计算机应用. 2012(07)
[10]CTCS-1级列控系统车载设备研发探讨[J]. 宫建基. 铁路技术创新. 2012(02)
博士论文
[1]基于SCBM的安全分析方法及其在列控系统中的应用[D]. 周果.北京交通大学 2016
硕士论文
[1]基于CSP的PSTM框架形式化分析与验证[D]. 刘艾伦.华东师范大学 2018
[2]基于TCPN的CTCS-1级列控系统RDC形式化建模与分析[D]. 徐越.北京交通大学 2018
[3]列控数据计算机辅助设计与验证方法研究[D]. 冯丹颖.北京交通大学 2018
[4]基于CSP的CBTC系统区域控制器的建模与验证[D]. 朱葛.北京交通大学 2014
[5]基于UPPAAL的CBTC系统数据验证的研究[D]. 王森.北京交通大学 2013
[6]基于STATEMATE的无线闭塞中心数据流生成及形式化验证[D]. 秦玲.北京交通大学 2009
[7]Petri网的改良可达树及可达性判定[D]. 邱经华.山东科技大学 2004
本文编号：3178896
【文章来源】：北京交通大学北京市 211工程院校 教育部直属院校
【文章页数】：111 页
【学位级别】：硕士
【文章目录】：
致谢
摘要
ABSTRACT
1 引言
1.1 研究背景和意义
1.1.1 研究背景
1.1.2 选题目的及意义
1.2 数据验证研究现状
1.2.1 列控系统数据验证研究现状
1.2.2 其他领域数据验证研究现状
1.3 CTCS-1级列控系统概述
1.4 论文的研究内容和框架
2 数据验证的理论基础
2.1 数据设计模型概述
2.2 通信顺序进程形式化建模方法
2.2.1 CSP方法概述
2.2.2 通信顺序进程CSP语义和语法
2.3 CSP模型-Petri网模型转换方法
2.3.1 Petri网基本概念
2.3.2 CSP-Petri网模型转换规则
2.4 本章小结
3 RDC静态数据生成
3.1 RDC概述
3.2 RDC静态数据需求分析
3.3 RDC数据组织方式分析
3.4 RDC静态数据模型建立
3.5 RDC静态数据生成实例
3.6 本章小结
4 RDC数据验证CSP模型的建立
4.1 RDC数据验证总体框架
4.2 RDC数据建模验证的总体思路
4.3 数据约束规则提取和验证方法设计
4.3.1 数据约束规则提取
4.3.2 约束规则管理
4.3.3 数据验证方法设计
4.4 数据验证CSP模型
4.4.1 数据验证总体模型
4.4.2 验证轨道区段数据CSP模型
4.4.3 验证进路数据CSP模型
4.5 本章小结
5 数据验证模型的形式化验证
5.1 模型检验方法
5.2 验证工具ProB
5.2.1 ProB概述
5.2.2 CSP_M语言转换
5.3 CSP语义模型检验
5.3.1 性质验证分析
5.3.2 数据验证模型正确性检验
5.3.3 数据验证模型功能性检验
5.3.4 数据验证模型安全性检验
5.3.5 验证结果分析
5.4 本章小结
6 RDC数据自动化验证工具的设计与实现
6.1 需求分析
6.2 软件设计
6.2.1 软件总体设计
6.2.2 数据审核逻辑模块详细设计
6.3 软件实现
6.3.1 开发环境
6.3.2 软件主界面
6.4 实际线路数据验证
6.5 本章小结
7 结论
7.1 总结
7.2 展望
参考文献
图索引
表索引
作者简历及攻读硕士学位期间取得的研究成果
学位论文数据集
【参考文献】：
期刊论文
[1]高速铁路产业发展的区域布局研究——基于中国铁路中长期发展规划政策[J]. 闫昱霖. 经济师. 2017(11)
[2]列车运行控制数据校核及管理系统[J]. 吕瑞,马春英. 铁道通信信号. 2017(02)
[3]基于SAT的应答器工程数据逻辑规则提取及验证[J]. 王彤典,赵会兵. 铁道学报. 2017(02)
[4]CTCS-1级列控系统总体技术方案探讨[J]. 莫志松. 中国铁路. 2016(08)
[5]城轨计算机联锁的数据安全性验证[J]. 周果,赵会兵. 铁道学报. 2016(08)
[6]列控工程数据自动审核的研究与实现[J]. 陈倩佳,卢佩玲. 铁路计算机应用. 2015(03)
[7]CTCS-0列控系统改造方案研究[J]. 黄玉祥. 中国铁路. 2014(09)
[8]基于进程迹的CSP模型验证框架[J]. 赵岭忠,翟仲毅,钱俊彦. 计算机科学. 2013(11)
[9]列控数据完备性建模方法研究[J]. 程忆佳,王俊峰. 铁路计算机应用. 2012(07)
[10]CTCS-1级列控系统车载设备研发探讨[J]. 宫建基. 铁路技术创新. 2012(02)
博士论文
[1]基于SCBM的安全分析方法及其在列控系统中的应用[D]. 周果.北京交通大学 2016
硕士论文
[1]基于CSP的PSTM框架形式化分析与验证[D]. 刘艾伦.华东师范大学 2018
[2]基于TCPN的CTCS-1级列控系统RDC形式化建模与分析[D]. 徐越.北京交通大学 2018
[3]列控数据计算机辅助设计与验证方法研究[D]. 冯丹颖.北京交通大学 2018
[4]基于CSP的CBTC系统区域控制器的建模与验证[D]. 朱葛.北京交通大学 2014
[5]基于UPPAAL的CBTC系统数据验证的研究[D]. 王森.北京交通大学 2013
[6]基于STATEMATE的无线闭塞中心数据流生成及形式化验证[D]. 秦玲.北京交通大学 2009
[7]Petri网的改良可达树及可达性判定[D]. 邱经华.山东科技大学 2004
本文编号：3178896
本文链接：https://www.wllwen.com/kejilunwen/daoluqiaoliang/3178896.html
