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

摘要

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

目录

声明

致谢

摘要

1 引言

1．1 选题背景及意义

1．1．1 列控系统概述

1．1．2 列控安全计算机的应用

1．1．3 本文研究意义

1．2 国内外研究现状

1．3 论文研究内容和组织结构

1．4 本章小结

2 列控安全计算机管理机制设计

2．1 列控安全计算机概述

2．1．1 列控安全计算机功能需求

2．1．2 既有列控安全计算机平台结构

2．1．3 下一代列控安全计算机结构

2．2 列控安全计算机控制原理

2．2．1 列控安全计算机功能描述

2．2．2 基于通信的任务级同步策略

2．2．3 数据比较功能

2．3 系统运行流程

2．3．1 主备状态切换流程

2．3．2 管理单元运行流程

2．4 本章小结

3 安全计算机管理机制的形式化验证

3．1 形式化验证方法

3．1．1 模型检验原理及步骤

3．1．2 CTL计算树逻辑概述

3．1．3 模型检测工具

3．2 管理单元的SMV建模

3．2．1 管理单元状态模型

3．2．2 程序结构及模型转换规则

3．3 验证结果分析

3．4 本章小结

4 安全计算机管理单元的实现与测试

4．1 管理单元的硬件设计与实现

4．1．1 管理单元的硬件结构和功能

4．1．2 硬件各模块的设计

4．1．3 PCB电路板的实现

4．2 状态机的设计与软件实现

4．2．1 安全软件的实现

4．2．2 状态机软件程序实现

4．3 调试环境设计与实现

4．4 测试结果分析

4．5 本章小结

5 结论

5．1 总结

5．2 展望

参考文献

附录

图索引

表索引

作者简历及攻读硕士学位期间取得的研究成果

学位论文数据集