CTCS-3级列控系统的UML建模与模型检验研究
| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-11页 |
| 1 引言 | 第11-20页 |
| ·选题背景及意义 | 第11-12页 |
| ·CTCS-3级列控系统简介 | 第12-14页 |
| ·关键技术介绍 | 第14-17页 |
| ·UML建模技术 | 第14-15页 |
| ·符号模型检验系统 | 第15页 |
| ·故障注入技术 | 第15-17页 |
| ·形式化验证集成的研究现状 | 第17页 |
| ·论文研究内容及组织结构 | 第17-20页 |
| 2 CTCS-3级列控系统的UML建模 | 第20-31页 |
| ·场景描述 | 第20-23页 |
| ·概述 | 第20页 |
| ·级间转换过程 | 第20-22页 |
| ·级间转换过程UML顺序图 | 第22-23页 |
| ·建立UML模型 | 第23-31页 |
| ·建立UML类图 | 第24-26页 |
| ·建立UML状态图 | 第26-31页 |
| 3 UML模型转换为SMV模型 | 第31-43页 |
| ·SMV语言介绍 | 第31-33页 |
| ·转换UML模型 | 第33-43页 |
| ·转换Balise类 | 第33-37页 |
| ·转换External_Event类 | 第37-38页 |
| ·转换OnBoardEquipment类 | 第38-40页 |
| ·Main模块 | 第40-43页 |
| 4 使用SMV检验系统性质 | 第43-53页 |
| ·计算树逻辑公式介绍 | 第43-45页 |
| ·检验SMV模型 | 第45-49页 |
| ·遇到的问题 | 第49-53页 |
| 5 SMV模型的安全性分析 | 第53-67页 |
| ·基于故障注入的安全性分析 | 第53-62页 |
| ·符号化故障树分析 | 第62-67页 |
| ·利用SMV生成故障树 | 第62-65页 |
| ·小结 | 第65-67页 |
| 6 总结与展望 | 第67-68页 |
| 参考文献 | 第68-71页 |
| 作者简历 | 第71-73页 |
| 学位论文数据集 | 第73页 |
