操作系统形式化设计与验证综述

Survey of Formal Design and Verification for Operating System

对操作系统的形式化设计和验证的概念进行介绍,描述其框架和基本方法。比较和分析操作系统宏内核和微内核结构,调查多个设计和验证项目,阐述项目的验证目标、方法、优缺点和进展情况。在总结研究现状的基础上,分析和展望操作系统形式化设计和验证的发展趋势,从操作系统模型设计、验证工具、代码实现和验证重用等方面给出形式化设计和验证的思路。

This paper introduces the concepts of formal design and verification for the Operating System（OS）,and elaborates the framework and foundational methods of formal design and verification.It compares and analyzes the monolithic kernel and micro kernel architectures of the OS.Meanwhile,it investigates multiple design and verification projects in depth,focusing on the verification objectives,the methodology,the advantages and limitations,and the progression.It summarizes the state of the art,analyzes and outlooks the trends of the formal design and verification for the OS.What is more,from the aspects of model design,verification tools,code implementation and verification reuse,it advances the ideas of formal design and verification.