| 摘要 | 第1-8页 |
| Abstract | 第8-12页 |
| 第一章 绪论 | 第12-28页 |
| ·操作系统验证相关工作 | 第17-18页 |
| ·面向目标代码的程序分析与验证方法现状 | 第18-20页 |
| ·程序验证与仿真工具现状 | 第20-23页 |
| ·现有问题 | 第23-25页 |
| ·本文的主要工作 | 第25-28页 |
| 第二章 面向嵌入式应用的目标代码中间语言xBIL | 第28-58页 |
| ·xBIL语言 | 第30-38页 |
| ·xBIL的操作语义 | 第38-44页 |
| ·xBIL的指称语义 | 第44-48页 |
| ·xBIL的语义等价性证明 | 第48-52页 |
| ·实时操作系统的xBIL表示与应用分析 | 第52-56页 |
| ·本章小结 | 第56-58页 |
| 第三章 xBIL位域运算与判定过程 | 第58-80页 |
| ·xBIL位域运算与判定过程的作用 | 第59-61页 |
| ·xBIL位域运算 | 第61-68页 |
| ·xBIL表达式的位域运算解释 | 第68-69页 |
| ·xBIL位域的公式的表示方法 | 第69-70页 |
| ·xBIL位域判定过程 | 第70-76页 |
| ·xBIL位域运算与判定过程应用示例 | 第76-79页 |
| ·本章小节 | 第79-80页 |
| 第四章 基于目标代码的实时操作系统API验证 | 第80-90页 |
| ·基于xBIL的霍尔逻辑断言表示与推理规则扩展 | 第80-84页 |
| ·基于霍尔逻辑的实时操作系统功能性验证 | 第84-88页 |
| ·本章小结 | 第88-90页 |
| 第五章 带概率的实时操作系统中断安全性质验证 | 第90-112页 |
| ·中断安全性质验证方法与流程 | 第91-92页 |
| ·xBIL中断抽象指令生成方法 | 第92-96页 |
| ·基于xBIL中断抽象指令的离散时间马尔科夫链建模 | 第96-102页 |
| ·中断安全性质与自动生成 | 第102-105页 |
| ·自动化验证 | 第105页 |
| ·ORIENTAIS中断安全性质验证结果 | 第105-110页 |
| ·本章小节 | 第110-112页 |
| 第六章 应用系统集成验证 | 第112-124页 |
| ·集成验证方法与流程 | 第114-116页 |
| ·形式化验证工具链平台 | 第116-120页 |
| ·自主开发工具 | 第120-122页 |
| ·本章小结 | 第122-124页 |
| 第七章 总结与展望 | 第124-126页 |
| 附录A | 第126-138页 |
| A.1 位域公式生成的判定命题1 | 第126-130页 |
| A.2 位域公式生成的判定命题2 | 第130-135页 |
| A.3 ORIENTAISAPI-GetAlarmxBIL | 第135-138页 |
| 参考文献 | 第138-148页 |
| 致谢 | 第148-150页 |
| 攻读博士学位期间发表论文、申请专利与参与科研项目情况 | 第150-152页 |
