| 中文摘要 | 第1-4页 |
| Abstract | 第4-12页 |
| 第一章 绪论 | 第12-16页 |
| ·研究背景及意义 | 第12-13页 |
| ·国内外研究现状 | 第13-14页 |
| ·本文研究内容 | 第14-15页 |
| ·本文组织结构 | 第15-16页 |
| 第二章 统一建模语言UML2.0 | 第16-26页 |
| ·引言 | 第16-17页 |
| ·UML2.0 简介 | 第17-21页 |
| ·UML2.0 基本组成 | 第17-19页 |
| ·UML2.0 的时间机制 | 第19-21页 |
| ·UML2.0 顺序图 | 第21-23页 |
| ·UML2.0 状态图 | 第23-25页 |
| ·UML2.0 状态图的语法 | 第23-24页 |
| ·UML2.0 状态图的语义 | 第24-25页 |
| ·本章小结 | 第25-26页 |
| 第三章 时间自动机和UPPAAL 简介 | 第26-33页 |
| ·模型检测技术概述 | 第26页 |
| ·时间自动机简介 | 第26-28页 |
| ·时间自动机的语法 | 第27-28页 |
| ·时间自动机的语义 | 第28页 |
| ·时间自动机的乘积 | 第28页 |
| ·模型检测工具UPPAAL 简介 | 第28-32页 |
| ·时间自动机网络的语法 | 第29-30页 |
| ·时间自动机网络的语义 | 第30-31页 |
| ·UPPAAL 需求规范语言 | 第31-32页 |
| ·本章小结 | 第32-33页 |
| 第四章 UML2.0 顺序图到时间自动机网络的转化 | 第33-46页 |
| ·UML 顺序图的形式化分析 | 第33-36页 |
| ·UML2.0 顺序图对象自动机的构造 | 第36-42页 |
| ·UML 顺序图对象自动机的构造 | 第37-38页 |
| ·UML2.0 顺序图对象自动机的构造 | 第38-42页 |
| ·UML2.0 顺序图时间约束的提取 | 第42-45页 |
| ·本章小结 | 第45-46页 |
| 第五章 UML 状态图网络到时间自动机网络的转化 | 第46-55页 |
| ·UML 状态图网络 | 第46-48页 |
| ·UML2.0 状态图的扩展 | 第46-47页 |
| ·UML2.0 状态图的形式化定义 | 第47页 |
| ·UML 状态图网络的语法和语义 | 第47-48页 |
| ·UML 状态图网络到时间自动机网络的转化 | 第48-54页 |
| ·UML2.0 状态图的平坦化 | 第48-50页 |
| ·状态图网络到时间自动机网络的转化 | 第50-54页 |
| ·本章小结 | 第54-55页 |
| 第六章 实时软件动态行为模型一致性验证 | 第55-66页 |
| ·UML 一致性简介 | 第55-57页 |
| ·水平一致性和垂直一致性 | 第55-56页 |
| ·语法一致性和语义一致性 | 第56-57页 |
| ·语法一致性验证 | 第57页 |
| ·语义一致性验证 | 第57-63页 |
| ·行为一致性验证 | 第58-62页 |
| ·时间一致性验证 | 第62-63页 |
| ·相关工作比较 | 第63-65页 |
| ·本章小结 | 第65-66页 |
| 第七章 实例研究 | 第66-84页 |
| ·汽车档位控制系统说明 | 第66-67页 |
| ·汽车档位控制系统的需求 | 第67-69页 |
| ·汽车档位控制系统建模 | 第69-74页 |
| ·UML 顺序图模型 | 第71-72页 |
| ·UML 状态图网络模型 | 第72-74页 |
| ·UML2.0 顺序图模型时间对象自动机的构造 | 第74-76页 |
| ·UML 状态图网络模型到时间自动机网络的转化 | 第76-78页 |
| ·档位控制器系统动态行为模型一致性验证 | 第78-83页 |
| ·语法一致性验证 | 第79页 |
| ·行为一致性验证 | 第79-81页 |
| ·时间一致性验证 | 第81-83页 |
| ·本章小结 | 第83-84页 |
| 第八章 结束语 | 第84-86页 |
| ·本文工作总结 | 第84-85页 |
| ·进一步工作 | 第85-86页 |
| 参考文献 | 第86-91页 |
| 攻读硕士学位期间参加的科研项目和发表的论文 | 第91-92页 |
| 致谢 | 第92-93页 |
| 详细摘要 | 第93-95页 |