基于运行时验证的列控系统形式分析
| 致谢 | 第1-6页 |
| 摘要 | 第6-7页 |
| ABSTRACT | 第7-10页 |
| 1 引言 | 第10-17页 |
| ·选题的目的及意义 | 第10-11页 |
| ·CTCS-3级列车运行控制系统介绍 | 第11-12页 |
| ·形式化方法研究现状 | 第12-15页 |
| ·本文研究内容及组织结构 | 第15-16页 |
| ·本章小结 | 第16-17页 |
| 2 运行时验证的理论基础 | 第17-26页 |
| ·运行时验证特点 | 第17-20页 |
| ·传统验证方法的不足 | 第17-18页 |
| ·运行时验证的特点 | 第18-20页 |
| ·运行时验证方法 | 第20-23页 |
| ·线性时序逻辑LTL | 第23-25页 |
| ·基于有限序列的LTL语法 | 第23-24页 |
| ·基于有限序列的LTL语义 | 第24-25页 |
| ·本章小结 | 第25-26页 |
| 3 基于4真值LTL的运行时验证 | 第26-48页 |
| ·4真值LTL的语法及语义 | 第26-31页 |
| ·基于将来时态的LTL语义 | 第27-28页 |
| ·基于过去时态的LTL的语法及语义 | 第28-31页 |
| ·基于4真值LTL的公式重写算法 | 第31-39页 |
| ·基于4真值将来时态LTL的重写逻辑算法 | 第31-36页 |
| ·基于4真值过去时态LTL的重写逻辑算法 | 第36-39页 |
| ·运行时验证在Maude中的实现 | 第39-44页 |
| ·公式近似算法 | 第44-47页 |
| ·本章小结 | 第47-48页 |
| 4 案例分析 | 第48-60页 |
| ·运行时验证工具开发 | 第48-51页 |
| ·CTCS-3车地通信会晤建立的运行时验证 | 第51-55页 |
| ·车地通信会晤建立过程 | 第51-52页 |
| ·车地通信会晤建立过程的验证 | 第52-55页 |
| ·CTCS-3中RBC交接过程的运行时验证 | 第55-59页 |
| ·RBC交接过程 | 第56-57页 |
| ·RBC交接过程的验证 | 第57-59页 |
| ·本章小结 | 第59-60页 |
| 5 结论 | 第60-62页 |
| 参考文献 | 第62-65页 |
| 表目录 | 第65-66页 |
| 图目录 | 第66-67页 |
| 作者简历 | 第67-69页 |
| 学位论文数据集 | 第69页 |
