| 摘要 | 第1-6页 |
| Abstract | 第6-12页 |
| 第一章 导论 | 第12-18页 |
| ·概述 | 第12-14页 |
| ·课题研究的背景 | 第12-13页 |
| ·课题研究的目的、意义 | 第13-14页 |
| ·国内外研究现状 | 第14-16页 |
| ·计算机联锁系统软件技术的研究现状 | 第14-15页 |
| ·形式化方法在该领域的研究现状 | 第15-16页 |
| ·课题的研究内容和论文的章节安排 | 第16-18页 |
| ·研究内容 | 第16-17页 |
| ·论文的章节安排 | 第17-18页 |
| 第二章 形式化描述方法 | 第18-37页 |
| ·形式化方法 | 第18-21页 |
| ·形式化方法定义 | 第18-19页 |
| ·形式化规格 | 第19页 |
| ·形式化验证 | 第19-20页 |
| ·形式化方法优缺点 | 第20-21页 |
| ·UML统一建模语言 | 第21-25页 |
| ·UML的定义和内容 | 第21-22页 |
| ·UML的视图与图 | 第22-23页 |
| ·UML的优缺点 | 第23-25页 |
| ·Petri网 | 第25-32页 |
| ·Petri网的基本定义 | 第25-27页 |
| ·Petri网的性质 | 第27-28页 |
| ·高级Petril网 | 第28-31页 |
| ·Petri网的优缺点 | 第31-32页 |
| ·时间自动机 | 第32-36页 |
| ·自动机概述 | 第32页 |
| ·时间自动机原理 | 第32-33页 |
| ·时间自动机语义和语法 | 第33-34页 |
| ·时间自动机简例 | 第34-36页 |
| ·时间自动机的优点 | 第36页 |
| ·本章小结 | 第36-37页 |
| 第三章 铁路信号与计算机联锁软件规则 | 第37-55页 |
| ·铁路信号概述 | 第37-38页 |
| ·计算机联锁软件 | 第38-39页 |
| ·概述 | 第38页 |
| ·联锁功能 | 第38-39页 |
| ·联锁软件规则的形式化定义 | 第39-53页 |
| ·联锁软件规则的提取与描述 | 第39-43页 |
| ·联锁软件规则的UML描述 | 第43-49页 |
| ·联锁软件规则的Petri网描述 | 第49-53页 |
| ·联锁软件规则模型的分析比较 | 第53-54页 |
| ·本章小结 | 第54-55页 |
| 第四章 基于UPPAAL的联锁软件规则的描述和验证 | 第55-68页 |
| ·引言 | 第55页 |
| ·UPRAAL自动验证工具 | 第55-60页 |
| ·UPPAAL简介 | 第55页 |
| ·UPPAAL语义和语法 | 第55-56页 |
| ·基于UPPAAL建模的实例 | 第56-60页 |
| ·联锁软件规则的时间自动机模型化描述和验证 | 第60-67页 |
| ·道岔 | 第60-62页 |
| ·信号机 | 第62-63页 |
| ·进路的锁闭 | 第63-64页 |
| ·进路的建立 | 第64-66页 |
| ·进路的解锁 | 第66-67页 |
| ·本章小结 | 第67-68页 |
| 第五章 结束语 | 第68-70页 |
| ·文章解决的关键问题和创新点 | 第68页 |
| ·进一步的工作 | 第68-70页 |
| 参考文献 | 第70-73页 |
| 攻读硕士学位期间完成的论文 | 第73页 |