| 致谢 | 第1-6页 |
| 中文摘要 | 第6-8页 |
| ABSTRACT | 第8-15页 |
| 1 绪论 | 第15-29页 |
| ·研究背景 | 第15页 |
| ·列控系统技术发展 | 第15-17页 |
| ·机械化时代的列控系统 | 第16页 |
| ·电气化时代的列控系统 | 第16-17页 |
| ·计算机时代的列控系统 | 第17页 |
| ·列控系统的相关特性 | 第17-19页 |
| ·系统特性 | 第17-19页 |
| ·系统规范相关性质 | 第19页 |
| ·列控系统的形式化应用现状 | 第19-24页 |
| ·选题意义 | 第24-25页 |
| ·论文主要工作与章节安排 | 第25-29页 |
| 2 形式化建模与验证方法综述 | 第29-37页 |
| ·概述 | 第29页 |
| ·形式化建模方法 | 第29-34页 |
| ·基于模型的方法 | 第29-31页 |
| ·基于进程演算的方法 | 第31-32页 |
| ·基于网络的方法 | 第32页 |
| ·基于逻辑的方法 | 第32-33页 |
| ·形式化建模方法比较 | 第33-34页 |
| ·形式化验证方法 | 第34-36页 |
| ·模型检验 | 第34-35页 |
| ·定理证明 | 第35-36页 |
| ·本章小结 | 第36-37页 |
| 3 列控系统分层形式化建模与验证框架 | 第37-51页 |
| ·列控系统的层次化模型 | 第37-42页 |
| ·层次化建模理论 | 第37-38页 |
| ·列控系统分层建模依据 | 第38-40页 |
| ·列控系统的分层体系结构 | 第40-42页 |
| ·列控系统形式化建模目标 | 第42-44页 |
| ·列控系统的形式化验证目标 | 第44-47页 |
| ·列控系统功能分类 | 第44-46页 |
| ·列控系统的验证特性 | 第46-47页 |
| ·分层形式化建模与验证框架 | 第47-49页 |
| ·本章小结 | 第49-51页 |
| 4 基于HCSP和CHARON的列控系统分层形式化建模 | 第51-77页 |
| ·HCSP | 第51-56页 |
| ·HCSP的语法 | 第51-52页 |
| ·HCSP的语义 | 第52-56页 |
| ·CHARON | 第56-59页 |
| ·CHARON的语法 | 第56-58页 |
| ·CHARON的语义 | 第58-59页 |
| ·CTCS-3级列控系统分层形式化建模 | 第59-74页 |
| ·系统层的HCSP模型 | 第60页 |
| ·场景层的HCSP模型 | 第60-63页 |
| ·组件层的CHARON模型 | 第63-65页 |
| ·功能层的CHARON模型 | 第65-74页 |
| ·本章小结 | 第74-77页 |
| 5 基于HCSP的列控系统运营场景验证方法 | 第77-101页 |
| ·概述 | 第77页 |
| ·理论基础 | 第77-81页 |
| ·时间自动机理论 | 第77-79页 |
| ·混合自动机理论 | 第79-80页 |
| ·CTL、TCTL和ACTL | 第80-81页 |
| ·实时性建模与验证方法 | 第81-90页 |
| ·实时约束行为描述 | 第82-83页 |
| ·转换规则 | 第83-89页 |
| ·实时性的验证 | 第89-90页 |
| ·混合属性的建模与验证方法 | 第90-98页 |
| ·假设条件及转换定义 | 第90-92页 |
| ·转换规则 | 第92-97页 |
| ·混合属性的验证 | 第97-98页 |
| ·本章小结 | 第98-101页 |
| 6 案例分析 | 第101-125页 |
| ·RBC切换场景实时性的建模与验证 | 第101-113页 |
| ·场景的HCSP模型 | 第103-106页 |
| ·CHARON模型 | 第106-108页 |
| ·场景实时性的TCTL描述 | 第108-109页 |
| ·模型的验证 | 第109-113页 |
| ·行车许可场景的建模与验证 | 第113-123页 |
| ·场景的HCSP模型 | 第114-118页 |
| ·CHARON模型 | 第118-121页 |
| ·混合属性的ACTL描述 | 第121页 |
| ·模型的验证 | 第121-123页 |
| ·本章小结 | 第123-125页 |
| 7 总结与展望 | 第125-129页 |
| ·论文工作总结 | 第125-126页 |
| ·未来工作展望 | 第126-129页 |
| 参考文献 | 第129-135页 |
| 附录A 行车许可场景的转换过程 | 第135-138页 |
| 附录B 行车许可场景的PHAVer模型 | 第138-141页 |
| 作者简历 | 第141-145页 |
| 学位论文数据集 | 第145页 |