| 摘要 | 第4-5页 |
| Abstract | 第5-6页 |
| 第一章 引言 | 第11-15页 |
| 1.1 研究背景 | 第11-12页 |
| 1.2 微内核 | 第12-13页 |
| 1.3 Isabelle/HOL介绍 | 第13-14页 |
| 1.4 本文研究内容以及主要工作 | 第14页 |
| 1.5 论文组织结构 | 第14-15页 |
| 第二章 相关工作介绍 | 第15-22页 |
| 2.1 微内核操作系统的发展 | 第15-17页 |
| 2.1.1 Mach | 第15页 |
| 2.1.2 L4 | 第15-16页 |
| 2.1.3 Minix | 第16-17页 |
| 2.2 操作系统验证项目的介绍 | 第17-22页 |
| 2.2.1 UCLA secure unix | 第17-19页 |
| 2.2.2 KIT | 第19页 |
| 2.2.3 VFiasco | 第19页 |
| 2.2.4 verisoft | 第19-21页 |
| 2.2.5 L4.verified | 第21-22页 |
| 第三章 VTOS中断及调度系统的设计与实现 | 第22-42页 |
| 3.1 系统架构 | 第22页 |
| 3.2 中断系统的实现 | 第22-38页 |
| 3.2.1 中断相关知识 | 第24-27页 |
| 3.2.2 VTOS的中断机制 | 第27-38页 |
| 3.3 调度系统的实现 | 第38-42页 |
| 3.3.1 VTOS的调度策略 | 第39-40页 |
| 3.3.2 enqueue()入队列 | 第40页 |
| 3.3.3 dequeue()出队列 | 第40-42页 |
| 第四章 中断及调度系统的验证 | 第42-76页 |
| 4.1 验证目标 | 第42-44页 |
| 4.2 霍尔逻辑 | 第44页 |
| 4.3 自动机理论 | 第44-47页 |
| 4.3.1 M_(VTOS) | 第45-46页 |
| 4.3.2 M_(Isabelle/HOL) | 第46-47页 |
| 4.3.3 M_(VTOS)与M_(Isabelle/HOL)的一致性 | 第47页 |
| 4.4 验证思想 | 第47-49页 |
| 4.5 Isabelle/HOL中的模型 | 第49-53页 |
| 4.5.1 中断描述符表 | 第49页 |
| 4.5.2 寄存器现场 | 第49-50页 |
| 4.5.3 进程结构体 | 第50-51页 |
| 4.5.4 中断函数链 | 第51页 |
| 4.5.5 系统的状态 | 第51-53页 |
| 4.6 定理的描述以及证明 | 第53-76页 |
| 4.6.1 IDT表的正确设置 | 第53-54页 |
| 4.6.2 上下文的保存 | 第54-56页 |
| 4.6.3 中断处理相关函数的验证 | 第56-74页 |
| 4.6.4 上下文的恢复 | 第74-76页 |
| 第五章 总结与展望 | 第76-78页 |
| 5.1 本文总结 | 第76页 |
| 5.2 本文的不足与展望 | 第76-78页 |
| 参考文献 | 第78-81页 |
| 致谢 | 第81-82页 |
| 攻读硕士学位期间参与的科研课题 | 第82-83页 |