| 中文摘要 | 第1-4页 |
| Abstract | 第4-7页 |
| 第一章 绪论 | 第7-12页 |
| ·论文研究背景 | 第7-8页 |
| ·国内外研究现状 | 第8-10页 |
| ·本文研究内容 | 第10-11页 |
| ·本文组织结构 | 第11-12页 |
| 第二章 实时系统与形式化方法 | 第12-25页 |
| ·实时系统概述 | 第12-14页 |
| ·实时系统的分类 | 第13页 |
| ·实时系统的特征 | 第13-14页 |
| ·形式化方法简介 | 第14-24页 |
| ·形式化描述（formal specification） | 第15-17页 |
| ·形式化验证 | 第17-24页 |
| ·本章小结 | 第24-25页 |
| 第三章 时间自动机及其验证工具UPPAAL | 第25-35页 |
| ·时间自动机 | 第25-30页 |
| ·转换系统与带时间约束的转换系统 | 第26-27页 |
| ·时间自动机的定义 | 第27-28页 |
| ·时间自动机简例 | 第28-29页 |
| ·时间自动机积的构造 | 第29-30页 |
| ·时间自动机验证工具UPPAAL | 第30-34页 |
| ·UPPAAL 的系统结构 | 第30-31页 |
| ·UPPAAL 中的查询语言 | 第31-32页 |
| ·UPPAAL 中的位置 | 第32-33页 |
| ·UPPAAL 中的时间自动机定义 | 第33-34页 |
| ·本章小结 | 第34-35页 |
| 第四章 统一建模语言UML 及其转换 | 第35-50页 |
| ·UML 概述 | 第35-39页 |
| ·UML 视图分析 | 第36-38页 |
| ·UML 顺序图 | 第38-39页 |
| ·UML 扩展机制 | 第39-44页 |
| ·UML 到时间自动机的转换 | 第44-49页 |
| ·简单子片段 | 第44页 |
| ·组合片段 | 第44-47页 |
| ·复合子片段 | 第47页 |
| ·时间自动机的优化 | 第47-49页 |
| ·本章小结 | 第49-50页 |
| 第五章 实例分析 | 第50-60页 |
| ·咖啡机控制系统描述与分析 | 第50-55页 |
| ·咖啡机控制系统说明 | 第50-51页 |
| ·咖啡机控制系统的UML 顺序图 | 第51页 |
| ·咖啡机控制系统的时间自动机模型 | 第51-54页 |
| ·咖啡机控制系统的分析与性质验证 | 第54-55页 |
| ·行人优先可控交通灯控制系统描述与分析 | 第55-59页 |
| ·交通灯控制系统说明 | 第55页 |
| ·交通灯控制系统UML 顺序图 | 第55-56页 |
| ·交通灯控制系统的时间自动机模型 | 第56-58页 |
| ·交通灯控制系统的分析与性质验证 | 第58-59页 |
| ·本章小结 | 第59-60页 |
| 第六章 总结与展望 | 第60-62页 |
| ·本文主要工作总结 | 第60页 |
| ·进一步的工作展望 | 第60-62页 |
| 参考文献 | 第62-67页 |
| 攻读硕士学位期间参加的科研项目和公开发表的论文 | 第67-68页 |
| 致谢 | 第68-69页 |
| 详细摘要 | 第69-71页 |