| 摘要 | 第5-7页 |
| Abstract | 第7-9页 |
| 第一章 绪论 | 第15-29页 |
| 1.1 实时系统模型检验技术 | 第15-22页 |
| 1.1.1 实时系统 | 第15-16页 |
| 1.1.2 中断驱动系统 | 第16-17页 |
| 1.1.3 软件系统的可靠性保障 | 第17-20页 |
| 1.1.4 模型检验技术 | 第20-22页 |
| 1.2 论文研究问题和目标 | 第22-26页 |
| 1.2.1 问题的提出 | 第22-24页 |
| 1.2.2 研究现状 | 第24-26页 |
| 1.3 论文的主要工作 | 第26-27页 |
| 1.4 论文的组织结构 | 第27-29页 |
| 第二章 本文研究工作相关技术介绍 | 第29-37页 |
| 2.1 时间自动机及时间自动机网络 | 第29-32页 |
| 2.2 时间自动机的可达性分析 | 第32-35页 |
| 2.3 时间自动机的有界模型检验方法 | 第35-37页 |
| 第三章 时间自动机可达性分析的偏序优化技术 | 第37-64页 |
| 3.1 背景 | 第37-38页 |
| 3.2 转换规划 | 第38-45页 |
| 3.2.1 独立转换 | 第38-39页 |
| 3.2.2 转换规划 | 第39-42页 |
| 3.2.3 使用转换规划的可达性分析 | 第42-45页 |
| 3.3 基于转换规划的偏序约减可达性分析算法 | 第45-59页 |
| 3.3.1 提前规划转换集合 | 第46-48页 |
| 3.3.2 扩展的偏序catch-up等价性以及相关算法 | 第48-53页 |
| 3.3.3 阻塞转换和优化偏序约减可达性算法实现 | 第53-55页 |
| 3.3.4 优化偏序约减可达性算法的正确性 | 第55-59页 |
| 3.4 案例分析 | 第59-62页 |
| 3.5 相关工作和小结 | 第62-64页 |
| 第四章 中断驱动控制系统的建模和模型转换技术 | 第64-79页 |
| 4.1 研究背景 | 第64-66页 |
| 4.2 任务加中断处理的中断驱动系统简介 | 第66-67页 |
| 4.3 和时序性质相关的系统要素信息 | 第67-69页 |
| 4.4 中断时间自动机和中断源建模 | 第69-73页 |
| 4.4.1 中断时间自动机 | 第69-70页 |
| 4.4.2 任务开始事件和中断事件的建模 | 第70-73页 |
| 4.5 中断向量表 | 第73页 |
| 4.6 中断处理程序模型和CPU处理栈模型 | 第73-76页 |
| 4.7 中断驱动系统的整体模型及其全局状态 | 第76-78页 |
| 4.8 小结 | 第78-79页 |
| 第五章 中断驱动控制系统的模型检验技术 | 第79-96页 |
| 5.1 事件路径 | 第79-80页 |
| 5.2 后继计算 | 第80-87页 |
| 5.2.1 计算全局状态上可能发生事件的集合 | 第81-82页 |
| 5.2.2 计算中断时间自动机的转换后继 | 第82-83页 |
| 5.2.3 计算中断向量表的事件后继 | 第83-85页 |
| 5.2.4 计算CPU处理栈内中断处理程序的事件后继 | 第85-86页 |
| 5.2.5 基于事件路径的超时检测 | 第86-87页 |
| 5.3 可达性分析算法 | 第87-92页 |
| 5.4 其他性质的验证 | 第92-93页 |
| 5.4.1 资源竞争验证 | 第92-93页 |
| 5.4.2 子程序原子性的验证 | 第93页 |
| 5.5 实例研究 | 第93-94页 |
| 5.6 相关工作和小结 | 第94-96页 |
| 第六章 中断驱动控制系统的有界模型检验技术 | 第96-120页 |
| 6.1 系统模型的扩展 | 第96-99页 |
| 6.2 有界模型检验算法的基本框架 | 第99-101页 |
| 6.2.1 不带时间信息的系统状态 | 第99-101页 |
| 6.2.2 有界模型检验算法的基本框架 | 第101页 |
| 6.3 状态的后继转换以及相应的后继状态 | 第101-109页 |
| 6.3.1 中断程序开始执行的事件 | 第102-103页 |
| 6.3.2 中断事件/任务调度自动机的后继事件 | 第103页 |
| 6.3.3 和中断处理程序执行相关的后继转换和后继状态 | 第103-109页 |
| 6.4 时间约束和规约的处理 | 第109-114页 |
| 6.4.1 时间约束的表示 | 第109-110页 |
| 6.4.2 各类转换的时间约束 | 第110-112页 |
| 6.4.3 状态对应的时间约束 | 第112-113页 |
| 6.4.4 时间规约的处理 | 第113-114页 |
| 6.5 使用SMT求解器实现对时间约束和规约的处理 | 第114-117页 |
| 6.5.1 SMT求解器Z3的相关命令的简介 | 第115-116页 |
| 6.5.2 使用Z3实现处理时间约束的方法 | 第116-117页 |
| 6.6 算法实现和反例显示 | 第117-118页 |
| 6.7 相关工作和小结 | 第118-120页 |
| 第七章 总结 | 第120-123页 |
| 参考文献 | 第123-132页 |
| 攻读博士期间发表的论文 | 第132-133页 |
| 致谢 | 第133-135页 |
