| 致谢 | 第1-5页 |
| 摘要 | 第5-7页 |
| ABSTRACT | 第7-17页 |
| 术语表 | 第17-18页 |
| 1. 引言 | 第18-30页 |
| ·研究背景 | 第18-19页 |
| ·城轨信号系统的结构和特点 | 第19-21页 |
| ·安全系统应用软件框架建模的内容和必要性 | 第21-22页 |
| ·形式化建模研究现状 | 第22-24页 |
| ·UML 语言 | 第23页 |
| ·Petri 网 | 第23-24页 |
| ·时间自动机 | 第24页 |
| ·模型驱动软件开发（MDSD）的国内外研究现状 | 第24-25页 |
| ·基于 MDA 的开发工具 | 第25-26页 |
| ·选题的目的和意义 | 第26页 |
| ·论文主要研究内容 | 第26-27页 |
| ·篇章结构 | 第27-30页 |
| 2. 模型驱动软件开发和软件质量评估的研究 | 第30-46页 |
| ·模型驱动软件开发 | 第30-37页 |
| ·MDSD 发展背景 | 第30-31页 |
| ·MDSD 的概念 | 第31页 |
| ·MDSD 和 MDA 的区别 | 第31-32页 |
| ·MDSD 术语 | 第32-35页 |
| ·软件体系结构 | 第35-36页 |
| ·以体系结构为中心的设计 | 第36-37页 |
| ·形式化方法 | 第37-40页 |
| ·形式化方法与软件形式化 | 第37-38页 |
| ·形式化方法与软件可靠性 | 第38-39页 |
| ·面向对象软件形式化方法 | 第39-40页 |
| ·软件评估 | 第40-43页 |
| ·软件质量评估 | 第40-42页 |
| ·软件可靠性评价 | 第42页 |
| ·软件可靠性测试过程 | 第42-43页 |
| ·软件评估体系的说明 | 第43-44页 |
| ·本章小结 | 第44-46页 |
| 3. 基于 UML 的模型定义及列控系统形式化建模 | 第46-68页 |
| ·UML 模型定义 | 第46-49页 |
| ·UML 语义及表示法 | 第46页 |
| ·UML 的分类及其模型图 | 第46-48页 |
| ·类图的定义 | 第48页 |
| ·状态图的定义 | 第48-49页 |
| ·序列图的定义 | 第49页 |
| ·UML 模型建立 | 第49-50页 |
| ·实例业务分析 | 第50-65页 |
| ·ATO 部分模块功能用例图 | 第52-55页 |
| ·ATO 部分模块功能类图 | 第55-59页 |
| ·ATO 部分模块功能状态图 | 第59-62页 |
| ·ATO 部分模块功能序列图 | 第62-65页 |
| ·本章小结 | 第65-68页 |
| 4. PETRI 网建模与测试案例验证 | 第68-134页 |
| ·PETRI 网的基本概念 | 第68-73页 |
| ·基本 Petri 网 | 第68-69页 |
| ·网的图形表示 | 第69页 |
| ·网系统 | 第69页 |
| ·Petri 网的动态性质 | 第69-71页 |
| ·Petri 网工作流程基本结构 | 第71-73页 |
| ·着色 PETRI 网（CPN）定义 | 第73-74页 |
| ·着色 Petri 网 | 第73-74页 |
| ·CPN 工具介绍 | 第74页 |
| ·验证技术 | 第74-80页 |
| ·模型检验 | 第75-77页 |
| ·测试序列集生成算法 | 第77-80页 |
| ·列车控制系统建模和验证实例 | 第80-94页 |
| ·线程模型方法 | 第81-86页 |
| ·对象模型方法 | 第86-94页 |
| ·UML 模型到 PETRI 网模型的转换 | 第94-110页 |
| ·UML 类图到 ObjCPN | 第94-97页 |
| ·UML 状态图到 ObjCPN | 第97-98页 |
| ·UML 序列图到 ThrCPN 及 ObjCPN | 第98-110页 |
| ·基于 OBJCPN 模型的层次化建模方法 | 第110-120页 |
| ·被测系统模型 | 第111-112页 |
| ·环境模型 | 第112-114页 |
| ·系统模型 | 第114-117页 |
| ·模型活性分析 | 第117-120页 |
| ·测试序列生成算法 | 第120-126页 |
| ·路径获取 | 第120-123页 |
| ·测试序列生成 | 第123-126页 |
| ·系统分析实例 | 第126-133页 |
| ·共享内存管理模块分析 | 第126-133页 |
| ·本章小结 | 第133-134页 |
| 5. 模型测试 | 第134-156页 |
| ·测试策略 | 第134-139页 |
| ·软件检验的方法 | 第134-135页 |
| ·软件测试工具介绍 | 第135-137页 |
| ·代码验证标准 | 第137-138页 |
| ·测试用例设计方法 | 第138-139页 |
| ·测试环境 | 第139页 |
| ·测试方案 | 第139-141页 |
| ·测试规程 | 第139-140页 |
| ·主要测试功能项 | 第140-141页 |
| ·测试过程 | 第141-149页 |
| ·模块结构分析 | 第141-146页 |
| ·静态测试 | 第146-148页 |
| ·动态测试 | 第148-149页 |
| ·测试结果 | 第149-153页 |
| ·串口模块测试结果 | 第149-150页 |
| ·ZC 接口模块的测试结果 | 第150-152页 |
| ·共享内存模块测试结果 | 第152-153页 |
| ·本章小结 | 第153-156页 |
| 6. 研究结论与展望 | 第156-159页 |
| ·研究结论 | 第156-157页 |
| ·本文创新点 | 第157页 |
| ·未来工作展望 | 第157-159页 |
| 参考文献 | 第159-168页 |
| 附录A 作者简历及科研成果清单 | 第168-170页 |
| 附录B 学位论文数据集 | 第170-171页 |
| 详细摘要 | 第171-184页 |