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

uqHZau

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

9 h1 ]3 f3 n$ b! L, a. \2 G
摘要:由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS( Verified Secure Operating System)内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述，并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.
9 ]6 {" U) u2 ?6 k关键词:操作系统;内存管理;形式化设计;形式化验证;定理证明
, J) g/ |* E% P& g3 H

1引言
" A$ w/ l8 K; D9 F$ a对于关键的核心软件系统如操作系统(OperatingSystem , OS),如何保证其正确可靠一直以来都是学术界和工业界努力的方向.形式化验证技术以数理逻辑为基础,具有严谨性的特点,目前被公认为是能够保证软件正确性的关键技术.形式化验证是指根据系统的规范或属性,使用形式化方法验证其正确性或非正确.
& @- K7 _; S& x# ?Verisoft是一个大型的计算机系统设计开发项目",目标在于对整个计算机系统自底向上从硬件层到应用软件层进行普适形式化证明( Pervasive Formal Verification).由于系统的庞大规模,内核部分验证所花费的人力和物力是巨大的,并且除内核外的其他模块并未得到完全验证[2].
) c6 W5 t! s+ C+ x+ u  d从上世纪90年代开始到现在,耶鲁大学ShaoZhong 教授带领的Flint项目组在形式化验证方面做了大量的工作[3,实现了一种新的逻辑编程语言Ver-iML[4],提出的入HOL Td逻辑加入了对数据类型的归纳定义,提供了丰富的形式化描述能力以及类型安全特性.同时, Flint 项目还研究了针对并行程序的验证方法[5],以及采用分层抽象的方法验证OS中的各种功能模块[6].

% U, j2 o- Z6 \3 u2 B" W

游客，如果您要查看本帖隐藏内容请回复

0 ^% E) B2 o. }6 f+ H# c" o: X. C

NingW

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