微内核架构内存管理的形式化设计和验证方法研究  

Research on Method of Formal Design and Verification of Memory Management Based on Microkernel Architecture

作　　者：钱振江[1,2] 刘永俊[2] 姚宇峰[2] 汤力[2] 黄皓[1] 宋方敏[1] 

机构地区：[1]南京大学计算机科学与技术系,江苏南京210023 [2]常熟理工学院计算机科学与工程学院,江苏苏州215500

出　　处：《电子学报》2017年第1期251-256,共6页Acta Electronica Sinica

基　　金：国家自然科学基金(No.61402057);江苏省科技计划自然科学研究项目(No.BK20140418);中国博士后科学基金(No.2015M571737);江苏省"六大人才高峰"高层次人才项目(No.2011-DZXX-035);江苏省高校自然科学研究项目(No.12KJB520001)

摘　　要：由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS(Verified Secure Operating System)内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.The correctness of design and implementation of operating systems is difficult to be described with the traditional quantitative methods,because of the enormous size and complexity. This paper illustrates our method of formal design and verification of microkernel operating system. We construct the system model with the non-deterministic automaton in the assembly level,and use the Hoare triples to describe the previous and post conditions of the interface functions,as the definitions of function correctness. We take the module of memory management in the self-implemented VSOS（ Verified Secure Operating System） as an example,to illustrate our formal method. Meanwhile,we formally describe the constructed memory management model and operation semantics of system behaviors in the Isabelle/HOL theorem prover,and verify the correctness of design and implementation of the memory management. The result shows that the method proposed is feasible and efficient.

关 键 词：操作系统 内存管理 形式化设计 形式化验证 定理证明 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]