| 摘要 | 第1-5页 |
| ABSTRACT | 第5-10页 |
| 缩略词 | 第10-11页 |
| 第一章 绪论 | 第11-19页 |
| ·引言 | 第11-12页 |
| ·嵌入式实时系统的建模与分析 MARTE | 第12-13页 |
| ·软件规约方法和 Z 语言 | 第13-15页 |
| ·软件规约方法概述 | 第13-14页 |
| ·软件规约语言 Z 语言 | 第14-15页 |
| ·接口自动机和时间自动机 | 第15-16页 |
| ·模型检测 | 第16-17页 |
| ·本文的主要研究内容和组织框架 | 第17-19页 |
| ·本文的主要究内容 | 第17页 |
| ·本文的组织框架 | 第17-19页 |
| 第二章 带 Z 的接口自动机 | 第19-23页 |
| ·接口自动机(IA) | 第19页 |
| ·时间自动机 | 第19页 |
| ·带 Z 的接口自动机(ZIA) | 第19-23页 |
| ·ZIA 的定义 | 第20-21页 |
| ·ZIA 之间的精化关系 | 第21-23页 |
| 第三章 从 MARTE 到 DT-ZIA 的转换 | 第23-38页 |
| ·MARTE | 第23-30页 |
| ·核心元素（Core Elements） | 第23-26页 |
| ·非功能性属性（Non-functional Properties） | 第26-28页 |
| ·时间（Time） | 第28-30页 |
| ·Z 语言 | 第30-31页 |
| ·UML 到 Z 的转换 | 第31-35页 |
| ·基于离散时间的 ZIA（DT-ZIA） | 第35页 |
| ·MARTE 的六元组表示 | 第35-36页 |
| ·MARTE 到 DT-ZIA 的转换 | 第36-38页 |
| 第四章 检测算法和实例验证 | 第38-73页 |
| ·ZIA 精化检测算法 | 第38-46页 |
| ·有限域的 ZIA | 第38-39页 |
| ·ZIA 精化检测算法 | 第39-41页 |
| ·ZIA 检测算法实现的主要数据结构 | 第41-43页 |
| ·算法流程图 | 第43-46页 |
| ·DT-ZIA 模型检测算法 | 第46-56页 |
| ·面向带有数据约束的实时系统时序逻辑 | 第47-51页 |
| ·有限域的 DT-ZIA | 第51-52页 |
| ·DT-ZIA 模型检测算法 | 第52-53页 |
| ·DT-ZIA 模型检测算法实现类图 | 第53-55页 |
| ·DT-ZIA 算法流程图 | 第55-56页 |
| ·实例验证 | 第56-73页 |
| ·ZIA 实例验证 | 第56-61页 |
| ·DT-ZIA 实例验证 | 第61-73页 |
| 第五章 总结和展望 | 第73-74页 |
| ·本文总结 | 第73页 |
| ·未来展望 | 第73-74页 |
| 参考文献 | 第74-76页 |
| 致谢 | 第76-77页 |
| 在学期间的研究成果及发表的学术论文 | 第77页 |