| 摘要 | 第1-5页 |
| Abstract | 第5-6页 |
| 目录 | 第6-8页 |
| 1 绪论 | 第8-12页 |
| ·论文的选题背景和研究意义 | 第8-9页 |
| ·国内外研究现状 | 第9-11页 |
| ·论文研究的主要内容 | 第11-12页 |
| 2 着色Petri网理论及验证工具 | 第12-17页 |
| ·形式化建模语言-着色Petri网 | 第12-15页 |
| ·Petri基本概念 | 第13-14页 |
| ·着色Petri定义 | 第14-15页 |
| ·CPN-Tools工具 | 第15-17页 |
| 3 行车许可模块设计与分析 | 第17-38页 |
| ·行车许可概述 | 第17-20页 |
| ·基于需求的功能模块划分 | 第20-22页 |
| ·行车许可生成原理 | 第22-25页 |
| ·基于功能需求的各应用层设计及分析 | 第25-38页 |
| ·完全监控模式下MA计算 | 第26-28页 |
| ·引导模式下MA计算 | 第28-29页 |
| ·等级转换模式下MA计算 | 第29-32页 |
| ·RBC切换模式下MA计算 | 第32-35页 |
| ·自动过分相区段MA计算 | 第35-36页 |
| ·临时限速下MA计算 | 第36-38页 |
| 4 基于着色Petri网的形式化建模 | 第38-49页 |
| ·顶层模型 | 第38-40页 |
| ·完全监控模式下MA生成过程建模 | 第40-42页 |
| ·等级转换模式下MA生成过程建模 | 第42-44页 |
| ·RBC切换模式下MA生成过程建模 | 第44-45页 |
| ·临时限速模式下MA生成过程建模 | 第45-46页 |
| ·赋时模型 | 第46-49页 |
| 5 基于CPN-Tools工具的仿真验证及性能分析 | 第49-58页 |
| ·状态空间分析 | 第49-55页 |
| ·性能分析 | 第55-58页 |
| 结论 | 第58-60页 |
| 致谢 | 第60-61页 |
| 参考文献 | 第61-64页 |
| 攻读学位期间的研究成果 | 第64页 |