1. INTRODUCTION

2. ANALYTICAL FRAMEWORK  
2.1. Concepts and Reference Architecture  
2.2. Separation Kernel Implementations  
2.3. Critical Properties and Standards  
2.4. Application Schema of Formal Methods  

3. TAXONOMY OF APPLYING FORMAL METHODS ON SEPARATION KERNELS  
3.1. Taxonomy  

4. ANALYSIS AND DISCUSSION  
4.1. Implementations  
4.2. Formal Specification and Model  
4.3. Critical Properties  
4.4. Formal Verification  
4.5. Code Abstraction  
4.6. Overall Comparison  

5. CHALLENGES AND FUTURE DIRECTIONS  
5.1. Eliminating Specification Bottleneck  
5.2. Automating Full Formal Verification  
5.3. Dealing with Multicore and Concurrency  
5.4. Formal Development and Code Generation  
5.5. Summary  

6. CONCLUSION