Survey of Formal Design and Verification for Operating System
Qian Zhen-jianga · Jisuanji gongcheng · 2012
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.