列控系统混成行为的建模与验证方法
| 致谢 | 第1-6页 |
| 中文摘要 | 第6-8页 |
| ABSTRACT | 第8-12页 |
| 1 引言 | 第12-20页 |
| ·选题目的及立题意义 | 第12-13页 |
| ·研究背景简介 | 第13-17页 |
| ·移动闭塞列车控制系统简介 | 第13-15页 |
| ·国内外形式化建模验证方法的研究现状 | 第15-16页 |
| ·国内外形式化验证工具集成平台研究现状 | 第16-17页 |
| ·论文的研究内容及组织结构 | 第17-18页 |
| ·本章小结 | 第18-20页 |
| 2 混成系统建模和验证方法介绍 | 第20-32页 |
| ·UML扩展机制 | 第20-21页 |
| ·面向混成行为的混UML概要文件设计 | 第21-25页 |
| ·数据类型概要文件 | 第21-22页 |
| ·类扩展概要文件 | 第22-23页 |
| ·表达式与约束概要文件 | 第23-24页 |
| ·扩展状态机概要文件 | 第24-25页 |
| ·混成自动机概述 | 第25-30页 |
| ·混成自动机的定义 | 第25-28页 |
| ·自动机之间的复合 | 第28-29页 |
| ·混成系统的可达性及安全性验证 | 第29-30页 |
| ·含有未知参数的线性混成自动机模型的安全性分析 | 第30页 |
| ·相关建模和验证工具介绍 | 第30-31页 |
| ·本章小结 | 第31-32页 |
| 3 非线性混成自动机时间有界的可达性分析方法 | 第32-44页 |
| ·时间有界的可达性分析方法 | 第32-33页 |
| ·可达性分析算法 | 第33-38页 |
| ·可达性分析算法基本流程 | 第34页 |
| ·可达性分析算法的伪代码表示 | 第34-38页 |
| ·HUML模型到HySAT模型的转换规则 | 第38-39页 |
| ·案例分析 | 第39-42页 |
| ·本章小结 | 第42-44页 |
| 4 未定参数分析方法 | 第44-56页 |
| ·未定参数分析方法基本流程 | 第44-45页 |
| ·案例分析 | 第45-54页 |
| ·移动闭塞系统 | 第46-47页 |
| ·建立移动闭塞追踪模型的线性混成自动机模型 | 第47-49页 |
| ·由HUML模型到HYTECH模型的转换规则 | 第49-51页 |
| ·验证HYTECH模型 | 第51-54页 |
| ·本章小结 | 第54-56页 |
| 5 混成自动机建模和验证工具集成 | 第56-64页 |
| ·工具集成的总体流程 | 第56-57页 |
| ·工具的实现过程及操作流程 | 第57-63页 |
| ·本章小结 | 第63-64页 |
| 6 结论 | 第64-66页 |
| 参考文献 | 第66-70页 |
| 附录：追踪模型案例的HYTECH模型 | 第70-74页 |
| 表目录 | 第74-76页 |
| 图目录 | 第76-78页 |
| 作者简历 | 第78-81页 |
| 学位论文数据集 | 第81页 |
