| 摘要 | 第1-11页 |
| ABSTRACT | 第11-13页 |
| 第一章 绪论 | 第13-21页 |
| ·实时系统、嵌入式系统和嵌入式软件 | 第13-14页 |
| ·形式化方法和模型检验技术 | 第14-16页 |
| ·时间自动机理论 | 第16-17页 |
| ·状态转换系统 | 第16页 |
| ·时间语言 | 第16-17页 |
| ·时间自动机 | 第17页 |
| ·WCET 技术 | 第17-18页 |
| ·论文主要研究内容 | 第18-19页 |
| ·论文结构 | 第19-21页 |
| 第二章 WCET 分析技术 | 第21-32页 |
| ·WCET 分析技术的发展历史和现状 | 第21页 |
| ·WCET 分析方法 | 第21-23页 |
| ·静态分析方法 | 第21-22页 |
| ·动态测量方法 | 第22页 |
| ·混合分析方法 | 第22-23页 |
| ·WCET 静态分析过程 | 第23-28页 |
| ·流分析 | 第24-27页 |
| ·低层分析 | 第27页 |
| ·WCET 计算 | 第27-28页 |
| ·典型的WCET 分析工具 | 第28-30页 |
| ·Bound-T | 第29页 |
| ·SWEET (SWEdish Execution Time tool) | 第29-30页 |
| ·RapiTime | 第30页 |
| ·CALC_WCET_167 | 第30页 |
| ·WCET 分析存在的问题 | 第30-31页 |
| ·本章小结 | 第31-32页 |
| 第三章 实时约束的执行路径映射 | 第32-53页 |
| ·程序代码的路径集划分 | 第32-43页 |
| ·划分的前提和约束 | 第32-33页 |
| ·划分过程 | 第33-43页 |
| ·处理结果 | 第43页 |
| ·实时约束的分析 | 第43-46页 |
| ·实时约束的描述 | 第44页 |
| ·状态时钟约束的获取 | 第44-45页 |
| ·实时约束的执行路径描述 | 第45-46页 |
| ·实时约束与路径集的映射 | 第46页 |
| ·实验 | 第46-52页 |
| ·预处理 | 第47-48页 |
| ·程序的基本块划分 | 第48-49页 |
| ·程序执行路径获取 | 第49-51页 |
| ·实时约束与函数集的映射 | 第51-52页 |
| ·本章小结 | 第52-53页 |
| 第四章 基于WCET 的模型检验方法 | 第53-71页 |
| ·基于WCET 分析的模型检验方法框架 | 第53-54页 |
| ·程序路径集的WCET 分析 | 第54-56页 |
| ·WCET 分析工具简介 | 第54-56页 |
| ·分析过程 | 第56页 |
| ·分析结果 | 第56页 |
| ·基于WCET 分析结果的实时模型建立和验证 | 第56-61页 |
| ·UPPAAL 简介 | 第56-58页 |
| ·基于UPPAAL 的建模过程 | 第58-59页 |
| ·实时性质验证 | 第59-61页 |
| ·实验 | 第61-70页 |
| ·实时约束的路径集划分 | 第62-64页 |
| ·映射路径集的WCET 分析 | 第64-66页 |
| ·模型修正 | 第66-67页 |
| ·基于程序分析的模型检验 | 第67-68页 |
| ·全系统的模型修正 | 第68-70页 |
| ·本章小结 | 第70-71页 |
| 第五章 面向中断的WCET 分析 | 第71-87页 |
| ·中断和WCET 分析 | 第71-75页 |
| ·中断和中断系统 | 第71-72页 |
| ·中断处理过程 | 第72-74页 |
| ·中断的WCET 分析 | 第74-75页 |
| ·面向中断的执行时间模型 | 第75-79页 |
| ·单重中断的时间性分析 | 第75-76页 |
| ·多重中断的时间性分析 | 第76-79页 |
| ·面向中断时间模型的WCET 计算 | 第79-81页 |
| ·单重中断 | 第80页 |
| ·多重中断 | 第80-81页 |
| ·实验 | 第81-86页 |
| ·单重中断处理程序的WCET 分析 | 第81-83页 |
| ·多重中断处理程序的WCET 分析 | 第83-84页 |
| ·中断处理对程序实时性的影响 | 第84-86页 |
| ·本章小结 | 第86-87页 |
| 第六章 基于WCET 分析的模型检验方法原型工具WCETModel | 第87-95页 |
| ·WCETModel 的功能和系统结构 | 第87-88页 |
| ·路径集划分PathAnalysis | 第88-90页 |
| ·实时约束映射ModeltoPath | 第90-91页 |
| ·WCETPath 和模型检验 | 第91-92页 |
| ·WCETInterrupt 和模型检验 | 第92-94页 |
| ·本章小结 | 第94-95页 |
| 结束语 | 第95-97页 |
| 致谢 | 第97-98页 |
| 参考文献 | 第98-102页 |
| 作者在学期间取得的学术成果 | 第102页 |