| 中文摘要 | 第1-4页 |
| ABSTRACT | 第4-8页 |
| 第一章 Introduction | 第8-11页 |
| ·Motivation | 第8-9页 |
| ·Thesis purpose and outline | 第9-10页 |
| ·Thesis structure | 第10-11页 |
| 第二章 Background | 第11-22页 |
| ·Model checking | 第11-17页 |
| ·General notion of finite state machine | 第12-13页 |
| ·A specific definition of finite state machine in our thesis | 第13-17页 |
| ·Bounded model checking | 第17-20页 |
| ·SMT solver Yices | 第20-22页 |
| 第三章 OSEK/VDX OS | 第22-26页 |
| ·History of OSEK/VDX | 第22页 |
| ·Operating system standard of OSEK/VDX | 第22-26页 |
| ·Task | 第22-23页 |
| ·Priority | 第23页 |
| ·Scheduling | 第23-26页 |
| 第四章 FPS model | 第26-32页 |
| ·Analysis FPS based on OSEK/VDX | 第26-28页 |
| ·Model for FPS | 第28-30页 |
| ·Definition for describing task behaviors | 第30-32页 |
| 第五章 Bounded model checking in the presence of Scheduler | 第32-45页 |
| ·Execution tree | 第32-38页 |
| ·Concept of execution tree | 第32-34页 |
| ·The algorithm for establishing a k-step execution tree | 第34-38页 |
| ·Two strategies for extracting execution paths | 第38-43页 |
| ·General Approach of Extracting Execution Paths (GAE2P) | 第39-41页 |
| ·Trim-tree Approach of Extracting Execution Paths (TAE2P) | 第41-43页 |
| ·Verification process with SMT tool Yices | 第43-45页 |
| 第六章 Verification tool | 第45-49页 |
| ·Architecture of verification tool | 第45-46页 |
| ·An example for using verification tool | 第46-49页 |
| 第七章 Experiments and evaluation | 第49-53页 |
| ·Experiments | 第49-51页 |
| ·Evaluation and discussion | 第51-53页 |
| 第八章 Related work | 第53-55页 |
| 第九章 Conclusion and future work | 第55-56页 |
| 参考文献 | 第56-59页 |
| 发表论文和科研情况说明 | 第59-60页 |
| 致谢 | 第60页 |
