基于CSP的城轨CBTC联锁逻辑形式化建模与验证
| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-10页 |
| 1 引言 | 第10-20页 |
| ·研究背景 | 第10-11页 |
| ·联锁系统概述 | 第11-14页 |
| ·城轨CBTC联锁子系统概述 | 第12-13页 |
| ·城轨CBTC联锁与传统联锁的比较 | 第13-14页 |
| ·本文的研究目的和意义 | 第14-16页 |
| ·形式化方法研究现状 | 第16-18页 |
| ·本文研究内容与体系结构 | 第18-20页 |
| ·本文研究框架 | 第18页 |
| ·本文的研究内容和结构 | 第18-20页 |
| 2 形式化方法与通信顺序进程 | 第20-34页 |
| ·形式化方法 | 第20-24页 |
| ·形式化方法概述 | 第20页 |
| ·形式化方法研究内容 | 第20-23页 |
| ·形式化方法分类 | 第23-24页 |
| ·通信顺序进程CSP | 第24-33页 |
| ·CSP概述 | 第24-25页 |
| ·CSP语义和语法 | 第25-33页 |
| ·小结 | 第33-34页 |
| 3 基于CSP的CBTC联锁逻辑建模与验证方法 | 第34-57页 |
| ·联锁的基本内容 | 第34-38页 |
| ·联锁的功能 | 第37页 |
| ·CBTC联锁的功能 | 第37-38页 |
| ·CBTC联锁进路控制逻辑建模 | 第38-50页 |
| ·基本进路的建立过程分析 | 第38-40页 |
| ·基本进路的CSP模型 | 第40-47页 |
| ·典型进路建模分析 | 第47-50页 |
| ·CBTC联锁逻辑的形式化验证 | 第50-56页 |
| ·ProB简介 | 第51-53页 |
| ·CSP_M语言 | 第53-54页 |
| ·性质验证分析 | 第54-56页 |
| ·小结 | 第56-57页 |
| 4 案例实现 | 第57-75页 |
| ·应用场景 | 第57-58页 |
| ·列车进路过程建模 | 第58-67页 |
| ·模型验证 | 第67-74页 |
| ·小结 | 第74-75页 |
| 5 总结和展望 | 第75-76页 |
| ·论文主要工作总结 | 第75页 |
| ·下一步工作展望 | 第75-76页 |
| 参考文献 | 第76-78页 |
| 图索引 | 第78-80页 |
| 表索引 | 第80-81页 |
| 作者简历 | 第81-83页 |
| 学位论文数据集 | 第83页 |
