VTOS内存管理的设计实现及其形式化验证研究

发布时间：2017-06-11 23:11

  本文关键词：VTOS内存管理的设计实现及其形式化验证研究，由笔耕文化传播整理发布。

【摘要】：计算机技术的发展使得计算机的应用领域日益扩大。在航天航空、轨道交通、医疗和金融等领域都可看见计算机的身影。计算机软件是计算机的灵魂,因此现代社会对计算机软件的依赖程度非常高。这种局面对软件的可靠性提出了很高的要求,社会对软件的高度依赖需要保证软件高度可靠。操作系统作为部署在计算机硬件之上的第一层软件,其可靠性至关重要,是其他软件可靠性的基础。传统的软件工程方法如测试等无法完全保证软件可靠,目前公认的能够保证软件正确可靠的技术是形式化验证技术。因此学习期间参加的项目组致力于开发一个基于微内核的操作系统VTOS (Verified Trusted Operating System),使用形式化验证技术保证其正确性。微内核具有封闭性的特点,且其小巧性使得形式化描述和验证成为可能。本文研究了VTOS中内存管理的设计实现及形式化验证方法,主要贡献如下：1、设计实现了VTOS的存储管理。在综合考虑微内核架构和系统的性能之后,提出并实现了将内存管理置于系统任务中的方案。按照功能将内存管理划分为页框分配器和进程虚存管理两个子模块。页框分配器负责页框的分配和释放,进程虚存管理负责管理进程的虚拟地址空间。2. VTOS内存管理模块的形式化建模。在考虑并发的情况下,利用非确定性自动机对实现的VTOS内存管理模块进行形式化建模,使用Hoare三元组描述了每一个接口函数的语义。函数的语义作为验证的目标。3、形式化模型的Isabelle/HOL描述。在辅助定理证明器Isabelle/HOL中描述了为内存模块所建立的自动机模型：定义了模型的状态空间；定义了每一个接口函数的前置条件和后置条件。为验证奠定了基础。4, VTOS内存管理模块的形式化验证。对内存管理模块的形式化验证进行了探索,在认识到面向确定性自动机的验证方法不能解决并发问题后,给出了面向非确定性自动机的验证方法。使用新方法对页框释放函数free_pages做了验证尝试,总结了验证工作所获得的经验。
【关键词】：操作系统 微内核 内存管理 模块化 形式化验证
【学位授予单位】：南京大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP333.1;TP311.52
【目录】：

• 摘要4-5
• ABSTRACT5-12
• 第一章 绪论12-18
• 1.1 研究背景12-13
• 1.2 相关工作13-16
• 1.2.1 微内核13-14
• 1.2.2 操作系统的形式化验证14-16
• 1.3 本文工作16
• 1.4 内容安排16-18
• 第二章 VTOS内存模块的设计与实现18-33
• 2.1 VTOS的结构18-19
• 2.2 内存管理模块的设计19-23
• 2.3 页框分配器的实现23-26
• 2.3.1 数据对象23-25
• 2.3.2 接口函数25-26
• 2.4 进程虚存管理的实现26-32
• 2.4.1 数据对象27-29
• 2.4.2 接口函数29-32
• 2.5 本章小结32-33
• 第三章 内存模块的形式化建模33-61
• 3.1 建模方法33-37
• 3.1.1 并发与非确定性33-35
• 3.1.2 概念与工具35-36
• 3.1.3 模块化原则36-37
• 3.2 页框分配器的建模37-47
• 3.2.1 模型的数学语言描述37-42
• 3.2.2 模型的Isabelle/HOL描述42-47
• 3.3 进程虚存管理的建模47-60
• 3.3.1 模型的数学语言描述47-55
• 3.3.2 模型的Isabelle/HOL描述55-60
• 3.4 本章小结60-61
• 第四章 内存模块的形式化验证61-84
• 4.1 原验证方法及其存在的问题61-64
• 4.2 汇编级模型与状态映射64-71
• 4.2.1 汇编级模型的定义64-68
• 4.2.2 汇编级状态到抽象自动机状态的映射68-70
• 4.2.3 模型之间的同构性70-71
• 4.3 函数的验证71-81
• 4.3.1 函数的证明思路71-77
• 4.3.2 函数实现到Isabelle/HOL的翻译77-79
• 4.3.3 函数实现的正确性验证79-81
• 4.4 本章小结81-84
• 第五章 总结与展望84-85
• 5.1 总结84
• 5.2 展望84-85
• 致谢85-86
• 参考文献86-88

【共引文献】

中国期刊全文数据库 前3条

1 QIAN Zhenjiang;LIU Wei;HUANG Hao;;Research on Microkernel Integrity Semantics Model and Formal Verification[J];Chinese Journal of Electronics;2014年01期

2 王若川;杨孟飞;乔磊;;基于时间自动机的操作系统中断管理建模与验证[J];空间控制技术与应用;2014年04期

3 谭彦亮;杨桦;乔磊;;基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证[J];空间控制技术与应用;2014年04期

中国博士学位论文全文数据库 前1条

1 钱振江;安全操作系统形式化设计与验证方法研究[D];南京大学;2013年

中国硕士学位论文全文数据库 前2条

1 闫鑫;基于ARINC653标准的分区操作系统隔离性的验证研究[D];太原理工大学;2014年

2 官水旺;VTOS系统任务设计与形式化验证[D];南京大学;2014年

  本文关键词：VTOS内存管理的设计实现及其形式化验证研究，，由笔耕文化传播整理发布。

本文编号：442711