| 摘要 | 第1-5页 |
| Abstract | 第5-8页 |
| 插图索引 | 第8-9页 |
| 附表索引 | 第9-10页 |
| 第1章 绪论 | 第10-14页 |
| ·研究背景 | 第10页 |
| ·研究目的及意义 | 第10-11页 |
| ·研究内容 | 第11-12页 |
| ·本文主要工作 | 第12-13页 |
| ·本文组织结构 | 第13页 |
| ·小结 | 第13-14页 |
| 第2章 相关研究 | 第14-26页 |
| ·汽车电子系统 | 第14-16页 |
| ·车载操作系统 | 第16-18页 |
| ·车载操作系统标准 OSEK | 第16页 |
| ·SmartOSEK 操作系统 | 第16-18页 |
| ·嵌入式系统实时性验证方法论 | 第18-25页 |
| ·形式化推理方法 | 第19页 |
| ·时间自动机建模 | 第19-23页 |
| ·AADL 建模 | 第23-25页 |
| ·小结 | 第25-26页 |
| 第3章 基于时间 Petri 网的汽车电子系统实时性验证方法 | 第26-38页 |
| ·时间 Petri 网 | 第26-28页 |
| ·时间 Petri 网建模具有的性质 | 第28-31页 |
| ·基于时间 Petri 网的实时性验证方法 | 第31-37页 |
| ·汽车电子系统的描述 | 第31页 |
| ·状态转换图到时间 Petri 网的映射规则 | 第31-32页 |
| ·Petri 网的优化策略 | 第32-36页 |
| ·汽车电子系统的实时性问题分析 | 第36页 |
| ·时间 Petri 网验证系统实时性的步骤 | 第36-37页 |
| ·小结 | 第37-38页 |
| 第4章 实例设计及实时性验证模型 | 第38-51页 |
| ·SkyEye 硬件模拟平台 | 第38-39页 |
| ·汽车自适应巡航控制系统（ACC）的设计实现 | 第39-45页 |
| ·ACC 系统简介 | 第39-40页 |
| ·ACC 系统的设计 | 第40-44页 |
| ·ACC 系统的实现 | 第44-45页 |
| ·ACC 系统分步建模 | 第45-47页 |
| ·建模工具 EXSPECT | 第47-48页 |
| ·ACC 系统的时间 Petri 网模型 | 第48-50页 |
| ·小结 | 第50-51页 |
| 第5章 实时性分析与验证 | 第51-58页 |
| ·任务运行时间的测量 | 第51-52页 |
| ·ACC 系统的实时性验证 | 第52-53页 |
| ·实时性数据对比与分析 | 第53-57页 |
| ·小结 | 第57-58页 |
| 结论 | 第58-60页 |
| 参考文献 | 第60-64页 |
| 致谢 | 第64-65页 |
| 附录 A 攻读硕士学位期间所发表的学术论文 | 第65-66页 |
| 附录 B 攻读硕士学位期间所参与的科研项目 | 第66-67页 |