列控安全计算机管理机制的形式化验证与实现

发布时间：2017-06-02 09:24

  本文关键词：列控安全计算机管理机制的形式化验证与实现，由笔耕文化传播整理发布。

【摘要】：随着近年来区域经济一体化的逐步形成,城市间人员流动的加快,基于传统架构的列车运行控制系统逐渐显露出不足。为满足人们出行快速、便捷的需求,在保证安全性和运输效率的同时,提高对多种系统运行平台的兼容性,针对下一代列控系统的研究已经展开。作为实现数据运算处理功能的载体,列控安全计算机一直是列控系统研究工作的关键部分。管理单元作为系统内部的中枢神经,主要实现安全计算机运行的管理机制,对运算协处理器以及安全输入输出单元进行调配,并对输出结果进行表决。而其中运行管理机制的验证与实现,对于列控安全计算机平台的构建具有十分重要的理论与实际意义。因此,本文旨在提出下一代列控安全计算机平台的结构与具体实现功能的基础上,对其中的管理机制进行验证,并进行管理单元的设计与实现。在对国内外列控系统进行研究的基础上,本文分析了下一代列控安全计算机功能需求,并对其内部结构进行详细说明,对集中式系统进行了结构上的改进,提出了分布式系统结构的下一代列控安全计算机设计方案,并对其管理域所实现的控制机制以及其原理进行设计,提出了内部单元的具体功能需求及运行流程。根据其所实现的管理功能,通过CTL操作符对相关性质进行描述,并以SMV描述语言对其进行状态机模型的建立,通过所选取的NuSMV形式化验证工具对其所实现的管理机制进行了相关性质的形式化验证,并对验证结果进行了分析,证明所设计的管理机制符合设计规范。硬件设计方面,基于差异性设计的原则,本文主要对管理域中基于MCU实现的管理单元进行设计。根据其具体的功能需求,完成了硬件相关模块的设计,并进行了MCU逻辑板PCB图的绘制。软件测试方面,通过编程对管理单元内部的状态机进行软件实现,并以PC机模拟FPGA逻辑板,实现其与MCU逻辑板的数据交互过程,通过设计的状态监测器对状态机内部进行监测。同时,以故障注入的方式对其所实现的状态转移功能进行了测试。通过对测试结果的分析,本文所设计与实现的基于MCU的管理单元能够实现预期的控制机制,实现了最初的设计目标。
【关键词】：列控 安全计算机 管理机制 形式化验证 设计与实现
【学位授予单位】：北京交通大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：U284.48
【目录】：

• 致谢5-6
• 摘要6-7
• ABSTRACT7-11
• 1 引言11-19
• 1.1 选题背景及意义11-16
• 1.1.1 列控系统概述11-15
• 1.1.2 列控安全计算机的应用15-16
• 1.1.3 本文研究意义16
• 1.2 国内外研究现状16-18
• 1.3 论文研究内容和组织结构18
• 1.4 本章小结18-19
• 2 列控安全计算机管理机制设计19-37
• 2.1 列控安全计算机概述19-25
• 2.1.1 列控安全计算机功能需求19-20
• 2.1.2 既有列控安全计算机平台结构20-22
• 2.1.3 下一代列控安全计算机结构22-25
• 2.2 列控安全计算机控制原理25-28
• 2.2.1 列控安全计算机功能描述25-26
• 2.2.2 基于通信的任务级同步策略26-27
• 2.2.3 数据比较功能27-28
• 2.3 系统运行流程28-35
• 2.3.1 主备状态切换流程28-32
• 2.3.2 管理单元运行流程32-35
• 2.4 本章小结35-37
• 3 安全计算机管理机制的形式化验证37-71
• 3.1 形式化验证方法37-43
• 3.1.1 模型检验原理及步骤37-39
• 3.1.2 CTL计算树逻辑概述39-42
• 3.1.3 模型检测工具42-43
• 3.2 管理单元的SMV建模43-54
• 3.2.1 管理单元状态模型43-48
• 3.2.2 程序结构及模型转换规则48-54
• 3.3 验证结果分析54-70
• 3.4 本章小结70-71
• 4 安全计算机管理单元的实现与测试71-97
• 4.1 管理单元的硬件设计与实现71-84
• 4.1.1 管理单元的硬件结构和功能71
• 4.1.2 硬件各模块的设计71-82
• 4.1.3 PCB电路板的实现82-84
• 4.2 状态机的设计与软件实现84-88
• 4.2.1 安全软件的实现84-86
• 4.2.2 状态机软件程序实现86-88
• 4.3 调试环境设计与实现88-91
• 4.4 测试结果分析91-95
• 4.5 本章小结95-97
• 5 结论97-99
• 5.1 总结97-98
• 5.2 展望98-99
• 参考文献99-103
• 附录A103-105
• 图索引105-107
• 表索引107-108
• 作者简历及攻读硕士学位期间取得的研究成果108-110
• 学位论文数据集110

【相似文献】

中国期刊全文数据库 前10条

1 袁湘鄂;史增树;李智;;尽头式车站列控技术方案[J];铁道通信信号;2010年08期

2 程忆佳;王俊峰;;列控数据完备性建模方法研究[J];铁路计算机应用;2012年07期

3 康健;党建武;赵庶旭;;客运专线列控设备维修研究[J];中国铁路;2012年09期

4 康健;周振华;;基于费用最小的列控设备维修优化与仿真[J];铁道标准设计;2012年12期

5 魏方华;吴倩;刘澜;;一次模式曲线列控方式追踪间隔的模拟计算与优化设计[J];交通运输系统工程与信息;2007年03期

6 闫晓莉;;列控车载数据无线传输管理系统的运用[J];铁道通信信号;2012年09期

7 易磊;郭友强;;列控车载设备维护管理探讨[J];铁道通信信号;2013年03期

8 张恬;;浅析非安全通道传输列控安全信息的措施和方法[J];甘肃科技纵横;2008年04期

9 徐建军;;铁路客专枢纽列控地面设备布置方案研究[J];铁道通信信号;2011年11期

10 傅世善;;闭塞与列控概论——第一讲 区间闭塞[J];铁路通信信号工程技术;2004年05期

中国重要会议论文全文数据库 前3条

1 谢静高;石锐华;;客运专线列控系统技术方案的探讨[A];铁路客运专线建设技术交流会论文集[C];2005年

2 李桂月;张洲初;牛意坚;;GSM-R网络列控类数据传输业务的QoS测试[A];GSM-R移动通信及无线电管理学术会议论文集[C];2006年

3 徐伟;肖宝弟;;基于多任务融合的城轨车载维检系统的设计与实现[A];第七届中国智能交通年会优秀论文集——智能交通应用[C];2012年

中国重要报纸全文数据库 前2条

1 谭小兵邋苏元宏;我国首套铁路信号、列控地面系统试验成功[N];人民铁道;2007年

2 中国铁道科学研究院 蒋志勇;无线通信在高速铁路的应用[N];人民邮电;2012年

中国硕士学位论文全文数据库 前8条

1 张勇;列控设备开发项目安全风险管理研究[D];浙江工业大学;2014年

2 梁靓;列控安全计算机管理机制的形式化验证与实现[D];北京交通大学;2016年

3 魏方华;基于模式曲线列控方式的列车追踪行车模拟研究[D];西南交通大学;2005年

4 殷原;提速条件下山区铁路列控方式研究[D];西南交通大学;2007年

5 裴丽君;列控模型参数辨识及其在线学习算法研究[D];北京交通大学;2011年

6 陈耿钦;基于MAS的列控系统安全分析平台架构和关键算法研究[D];北京交通大学;2014年

7 薛辉;基于UML的车载列控显示系统的设计与实现[D];北京交通大学;2006年

8 李e，

本文编号：414807