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

作     者：钱振江 黄皓 宋方敏 QIAN Zhen-Jiang HUANG Hao SONG Fang-Min

作者机构：南京大学计算机科学与技术系江苏南京210023 常熟理工学院计算机科学与工程学院江苏苏州215500 King's College LondonLondon WC2R2LSUK 

基　　金：国家自然科学基金(61402057) 江苏省科技计划自然科学研究项目(BK20140418) 中国博士后科学基金(2015M571737) 江苏省“六大人才高峰”高层次人才项目(2011-DZXX-035) 江苏省高校自然科学研究项目(12KJB520001)~~ 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2016年第27卷第12期

页      码：3143-3157页

摘      要：由于系统的巨大规模,操作系统设计和实现的正确性很难用传统的方法进行描述和验证.在汇编层形式化地对系统模块的功能语义进行建模,提出一种汇编级的系统状态模型,作为汇编语言层设计和验证的纽带.通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域,并以此来描述汇编层的论域.通过验证汇编层的功能模块的正确性来保证汇编语言层设计的正确性,达到对系统功能实现的正确性验证.同时,使用定理证明工具Isabelle/HOL来形式化地描述这一系统状态模型,基于这一形式化模型,在Isabelle/HOL中验证系统模块的功能语义的正确性.以实现的安全可信OS(verified secure operating system,简称VSOS)为例,阐述了所提出的形式化设计和验证方法,说明了这一方法的可行性.

主 题 词：操作系统 正确性验证 形式化方法 系统状态模型 

学科分类：08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.13328/j.cnki.jos.004851

馆 藏 号：203209804...