| 致谢 | 第4-5页 |
| 中文摘要 | 第5-6页 |
| ABSTRACT | 第6-7页 |
| 术语表 | 第18-19页 |
| 1. 绪论 | 第19-33页 |
| 1.1 研究背景 | 第19-27页 |
| 1.1.1 问题的提出 | 第19-22页 |
| 1.1.2 相关概念 | 第22-27页 |
| 1.2 CBTC联锁系统建模与验证方法的演化 | 第27-29页 |
| 1.2.1 传统的建模与验证方法 | 第27页 |
| 1.2.2 基于形式化方法的建模与验证 | 第27-28页 |
| 1.2.3 组合形式化方法的形成 | 第28-29页 |
| 1.3 选题的意义和目的 | 第29-30页 |
| 1.4 论文主要内容与篇章结构 | 第30-33页 |
| 2. CBTC联锁系统的形式化建模与验证方法研究现状 | 第33-39页 |
| 2.1 联锁系统形式化建模方法综述 | 第33-35页 |
| 2.2 联锁系统形式化验证方法综述 | 第35-37页 |
| 2.3 研究现状总结与分析 | 第37-39页 |
| 2.3.1 研究现状总结 | 第37-38页 |
| 2.3.2 研究现状分析 | 第38-39页 |
| 3. 基于HCPN的CBTC联锁系统形式化建模方法 | 第39-69页 |
| 3.1 基本概念 | 第39-42页 |
| 3.1.1 Petri网 | 第39-40页 |
| 3.1.2 有色Petri网 | 第40页 |
| 3.1.3 分层有色Petri网 | 第40-41页 |
| 3.1.4 CPN Tools | 第41-42页 |
| 3.2 有色Petri网的形式化建模方法 | 第42-50页 |
| 3.2.1 非分层有色Petri网模型构建 | 第42-45页 |
| 3.2.2 分层有色Petri网（HCPN）模型构建 | 第45-47页 |
| 3.2.3 具有优先级的HCPN模型构建 | 第47-50页 |
| 3.3 CBTC联锁系统HCPN模型模板 | 第50-68页 |
| 3.3.1 CBTC联锁系统模板的顶层模型 | 第51-52页 |
| 3.3.2 CBTC联锁系统模板的外部接口对象模型 | 第52-59页 |
| 3.3.3 CBTC联锁系统模板的内部控制对象模型 | 第59-65页 |
| 3.3.4 CBTC联锁模板参数化 | 第65-68页 |
| 3.4 本章小结 | 第68-69页 |
| 4. 基于互斥锁和消息驱动的CBTC联锁系统形式化建模方法 | 第69-87页 |
| 4.1 相关概念 | 第69-72页 |
| 4.1.1 并发与同步触发 | 第69-70页 |
| 4.1.2 互斥锁 | 第70-72页 |
| 4.1.3 消息驱动 | 第72页 |
| 4.2 联锁系统中的并发与同步触发问题 | 第72-74页 |
| 4.2.1 问题描述 | 第72-73页 |
| 4.2.2 解决思路 | 第73-74页 |
| 4.3 实例分析 | 第74-86页 |
| 4.3.1 CPN模型 | 第74-77页 |
| 4.3.2 CPN模型分析 | 第77-79页 |
| 4.3.3 HCPN模型中并发性与同步触发的基本假设 | 第79-80页 |
| 4.3.4 互斥锁解决方案 | 第80-81页 |
| 4.3.5 消息驱动机制解决方案 | 第81-86页 |
| 4.4 本章小结 | 第86-87页 |
| 5. 模型转换：从CPN至B语言 | 第87-103页 |
| 5.1 B方法概述 | 第87-92页 |
| 5.1.1 B方法的符号表示 | 第88-90页 |
| 5.1.2 抽象机 | 第90-91页 |
| 5.1.3 B方法支持工具 | 第91-92页 |
| 5.2 CPN至B转换机制 | 第92-96页 |
| 5.2.1 CPN至B静态转换规则 | 第92-94页 |
| 5.2.2 CPN至B动态转换规则 | 第94-95页 |
| 5.2.3 CPN至B行为等价性 | 第95-96页 |
| 5.3 CPN至B实例验证 | 第96-101页 |
| 5.4 本章小结 | 第101-103页 |
| 6. 基于时间自动机的CBTC联锁系统形式化建模方法 | 第103-131页 |
| 6.1 时间自动机 | 第103-105页 |
| 6.2 联锁逻辑子系统的功能描述 | 第105-106页 |
| 6.3 联锁逻辑子系统主要场景建模 | 第106-125页 |
| 6.3.1 信号机控制模型 | 第106-109页 |
| 6.3.2 道岔控制 | 第109-114页 |
| 6.3.3 进路控制 | 第114-120页 |
| 6.3.4 屏蔽门控制 | 第120-124页 |
| 6.3.5 LEU控制 | 第124-125页 |
| 6.4 基于UPPALL的联锁逻辑子系统的分析和验证 | 第125-129页 |
| 6.4.1 仿真时序图 | 第125-128页 |
| 6.4.2 功能性验证 | 第128页 |
| 6.4.3 时间特性验证 | 第128-129页 |
| 6.4.4 安全性验证 | 第129页 |
| 6.5 本章小结 | 第129-131页 |
| 7. 结论与展望 | 第131-133页 |
| 7.1 研究成果 | 第131页 |
| 7.2 论文创新点 | 第131-132页 |
| 7.3 展望 | 第132-133页 |
| 参考文献 | 第133-141页 |
| 附录A | 第141-147页 |
| 附录B | 第147-155页 |
| 作者简历及科研成果 | 第155-158页 |
| 学位论文数据集 | 第158-159页 |
| 中文详细摘要 | 第159-172页 |
