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

发布时间：2018-02-25 08:04

  本文关键词： 操作系统 内存管理 形式化设计 形式化验证 定理证明　出处：《电子学报》2017年01期 　论文类型：期刊论文

【摘要】：由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS(Verified Secure Operating System)内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.
[Abstract]:Because of its size and complexity, The correctness of the design and implementation of the operating system is difficult to be described by the traditional quantitative method. This paper describes the formal design and verification methods of the microkernel operating system. In the assembly layer, the non-deterministic automata is used to model the system formally. The Hoare triple is used to describe the pre-and post-condition of the module interface function as the definition of the correctness of the function. The VSOS(Verified Secure Operating system memory management module is used as an example. In the Isabelle/HOL theorem prover environment, the established memory management model and the operational semantics of the system behavior are formally described, and the correctness of the design and implementation of the memory management module is verified. This method is feasible and efficient.
【作者单位】： 南京大学计算机科学与技术系;常熟理工学院计算机科学与工程学院;
【基金】：国家自然科学基金(No.61402057) 江苏省科技计划自然科学研究项目(No.BK20140418) 中国博士后科学基金(No.2015M571737) 江苏省“六大人才高峰”高层次人才项目(No.2011-DZXX-035) 江苏省高校自然科学研究项目(No.12KJB520001)
【分类号】：TP316

【相似文献】

相关期刊论文 前10条

1 古天龙;董荣胜;;欧洲高校计算机专业的形式化方法课程教学[J];计算机教育;2008年10期

2 柴振荣;《编程中的形式化方法及其应用》会议[J];管理科学文摘;1995年06期

3 郑士贵;智能服务网络形式化方法的模拟和实质[J];管理科学文摘;1997年01期

4 姜利;孙永强;;形式化方法的发展及展望[J];计算机科学;1998年02期

5 张广泉;关于软件形式化方法[J];重庆师范学院学报(自然科学版);2002年02期

6 鹿蕾;;形式化方法B的证明技术[J];现代电子技术;2005年23期

7 陈澎;设计模式形式化方法分析和初步比较[J];计算机工程;2005年02期

8 李建华;李红革;;形式化及其历史发展[J];自然辩证法研究;2008年08期

9 曹源;唐涛;徐田华;穆建成;;形式化方法在列车运行控制系统中的应用[J];交通运输工程学报;2010年01期

10 ;《软件学报》形式化方法和工具专刊征文通知[J];软件学报;2010年07期

相关会议论文 前7条

1 李文健;;形式化的涵义及其认识论本质[A];1993年逻辑研究专辑[C];1993年

2 吴允曾;;关于形式化的几个问题[A];金岳霖学术思想研究——金岳霖学术思想研讨会论文集[C];1985年

3 郑宇军;石海鹤;薛锦云;;Spec#语言中的形式化特性[A];2005年全国理论计算机科学学术年会论文集[C];2005年

4 雷敏;雷友殉;;一种UML到SDL转换方法的研究与应用[A];2006通信理论与技术新进展——第十一届全国青年通信学术会议论文集[C];2006年

5 苗洁君;王克;;密码模块的形式化设计和验证研究[A];第二十一次全国计算机安全学术交流会论文集[C];2006年

6 缪道期;;评审计算机安全等级[A];第二次计算机安全技术交流会论文集[C];1987年

7 赵晓峰;;城市轨道交通自主化信号系统全面创新实践[A];中国系统工程学会第十八届学术年会论文集——A12系统科学与系统工程理论在各个领域中的应用研究[C];2014年

相关重要报纸文章 前1条

1 殷杰 安军 山西大学科学技术哲学研究中心;21世纪科学哲学的关键词:语境、科学理性与形式化[N];中国社会科学报;2011年

相关博士学位论文 前8条

1 刘艳;互联网内容分级服务技术标准体系的形式化设计与验证[D];华中师范大学;2015年

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

3 刘强;设计模式的形式化研究及其EMF实现[D];华东师范大学;2011年

4 张鹏;形式化方法在云计算中的应用研究[D];吉林大学;2014年

5 刘洋;网络式软件需求验证的形式化方法研究[D];电子科技大学;2013年

6 王迈;语言形式化原理[D];上海外国语大学;2011年

7 胡静;基于Pi-演算的Web服务形式化描述模型[D];天津大学;2013年

8 周宁;代数化符号模拟验证的应用研究[D];北京交通大学;2015年

相关硕士学位论文 前10条

1 王春晓;MDF连续平压质量控制形式化建模及优化研究[D];东北林业大学;2015年

2 王亚丽;面向机器人规划的形式化研究[D];北京化工大学;2015年

3 韩佳芮;基于Event-B和MAS的车站进路联锁控制逻辑的形式化方法研究[D];兰州交通大学;2015年

4 徐世泽;基于Timed RAISE的RBC切换建模与分析[D];兰州交通大学;2015年

5 郭叶芳;电网控制系统软件可靠性分析的形式化方法研究[D];华北电力大学;2015年

6 黄峰;系统演化的形式化与具体化研究[D];南京邮电大学;2014年

7 温晋杰;Z规范对国产化软件工程实践的探讨[D];石家庄铁道大学;2016年

8 丁宁;基于要素投影的事件本体形式化方法及其在情感分析中的应用[D];上海大学;2016年

9 沈岗;基于UML的形式化框架及其在安全协议验证中的应用[D];天津大学;2014年

10 Hamza I.Bangura;基于Z规格的软件缺陷形式化方法[D];天津大学;2010年

，

本文编号：1533612