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