列控安全计算机管理机制的形式化验证与实现
致谢 | 第5-6页 |
摘要 | 第6-7页 |
ABSTRACT | 第7-8页 |
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页 |
附录A | 第103-105页 |
图索引 | 第105-107页 |
表索引 | 第107-108页 |
作者简历及攻读硕士学位期间取得的研究成果 | 第108-110页 |
学位论文数据集 | 第110页 |