操作系统汇编级形式化设计和验证方法

发布时间：2017-09-09 10:29

  本文关键词：操作系统汇编级形式化设计和验证方法

  更多相关文章： 操作系统 正确性验证 形式化方法 系统状态模型

【摘要】：由于系统的巨大规模,操作系统设计和实现的正确性很难用传统的方法进行描述和验证.在汇编层形式化地对系统模块的功能语义进行建模,提出一种汇编级的系统状态模型,作为汇编语言层设计和验证的纽带.通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域,并以此来描述汇编层的论域.通过验证汇编层的功能模块的正确性来保证汇编语言层设计的正确性,达到对系统功能实现的正确性验证.同时,使用定理证明工具Isabelle/HOL来形式化地描述这一系统状态模型,基于这一形式化模型,在Isabelle/HOL中验证系统模块的功能语义的正确性.以实现的安全可信OS(verified secure operating system,简称VSOS)为例,阐述了所提出的形式化设计和验证方法,说明了这一方法的可行性.
【作者单位】： 南京大学计算机科学与技术系;常熟理工学院计算机科学与工程学院;King’s
【关键词】： 操作系统 正确性验证 形式化方法 系统状态模型
【基金】：国家自然科学基金(61402057) 江苏省科技计划自然科学研究项目(BK20140418) 中国博士后科学基金(2015M571737) 江苏省“六大人才高峰”高层次人才项目(2011-DZXX-035) 江苏省高校自然科学研究项目(12KJB520001)~~
【分类号】：TP316
【正文快照】： 3(King’s College London,London WC2R 2LS,UK)www.jos.org.cn/1000-9825/4851.htm英文引用格式:Qian ZJ,Huang H,Song FM.Method of formal design and verification of OS on assembly layer.Ruan Jian XueBao/Journal of Software,2016,27(12):3143?3157(in Chinese).http

【相似文献】

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

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

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

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

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

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

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

7 王戟;李宣东;;形式化方法与工具专刊前言[J];软件学报;2011年06期

8 胡家宝，，姚干洲;形式化方法的回顾（续一）[J];计算机与现代化;1994年04期

9 郑红军;张乃孝;;软件开发中的形式化方法[J];计算机科学;1997年06期

10 柴振荣;形式化方法与软件的可靠性[J];管理科学文摘;1999年09期

中国重要会议论文全文数据库 前4条

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

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

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

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

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

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

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

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

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

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

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

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

3 钟琪;软件分析模式的形式化研究[D];西南师范大学;2004年

4 郭忠伟;神经内分泌复杂系统的形式化研究[D];扬州大学;2009年

5 王晓帆;基于模糊数学的形式化开发方法研究[D];西安理工大学;2003年

6 闵洪军;软件工程中形式化方法研究[D];浙江大学;2006年

7 张杨;UML模型形式化转换及验证的研究[D];太原理工大学;2013年

8 匡春临;并发系统的形式化技术研究[D];华侨大学;2008年

9 白锐;ATP系统形式化开发方法的研究[D];兰州交通大学;2014年

10 解方;从UML建模到Z形式化规范的研究[D];太原理工大学;2013年

本文编号：819915