主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
钱振江,黄皓,宋方敏.操作系统汇编级形式化设计和验证方法.软件学报,2016,27(12):3143-3157
操作系统汇编级形式化设计和验证方法
Method of Formal Design and Verification of OS on Assembly Layer
投稿时间:2014-06-10  修订日期:2015-04-03
DOI:10.13328/j.cnki.jos.004851
中文关键词:  操作系统  正确性验证  形式化方法  系统状态模型
英文关键词:operating system  correctness verification  formal method  system state model
基金项目:国家自然科学基金(61402057);江苏省科技计划自然科学研究项目(BK20140418);中国博士后科学基金(2015M571737);江苏省“六大人才高峰”高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)
作者单位E-mail
钱振江 南京大学 计算机科学与技术系, 江苏 南京 210023
常熟理工学院 计算机科学与工程学院, 江苏 苏州 215500
King's College London, London WC2R 2LS, UK 
tony_h@sina.com 
黄皓 南京大学 计算机科学与技术系, 江苏 南京 210023  
宋方敏 南京大学 计算机科学与技术系, 江苏 南京 210023  
摘要点击次数: 1030
全文下载次数: 1205
中文摘要:
      由于系统的巨大规模,操作系统设计和实现的正确性很难用传统的方法进行描述和验证.在汇编层形式化地对系统模块的功能语义进行建模,提出一种汇编级的系统状态模型,作为汇编语言层设计和验证的纽带.通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域,并以此来描述汇编层的论域.通过验证汇编层的功能模块的正确性来保证汇编语言层设计的正确性,达到对系统功能实现的正确性验证.同时,使用定理证明工具Isabelle/HOL来形式化地描述这一系统状态模型,基于这一形式化模型,在Isabelle/HOL中验证系统模块的功能语义的正确性.以实现的安全可信OS(verified secure operating system,简称VSOS)为例,阐述了所提出的形式化设计和验证方法,说明了这一方法的可行性.
英文摘要:
      The correctness of design and implementation of operating system is difficult to be described and verified with the traditional methods, due to the huge size of the system. In this paper, a model is build for the functionality semantics of the system modules on the assembly layer. A system state model is proposed as the link of the design and verification on the assembly layer. Through defining the legal states and state transition functions, the universe of discourse of the system state model and the assembly layer are constructed. The correctness of functionality modules is verified to ensure the correctness of design and functionality implementation. Within the Isabelle/HOL theorem prover, the system state model is described, and the correctness of functionality semantics of the system modules is verified. Meanwhile, the self-implemented secure trusted operating system (verified secure operating system, VSOS) is used as the example to illustrate the proposed formal method for design and verification, and to show the feasibility of the method.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利