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

来源：软件学报杂志2016年第12期北京时间：

作者：钱振江,黄皓,宋方敏

单位：钱振江，南京大学 计算机科学与技术系, 江苏 南京 210023;常熟理工学院 计算机科学与工程学院, 江苏 苏州 215500;Kings College London, London WC2R 2LS, UK11,黄皓，南京大学 计算机科学与技术系, 江苏 南京 21002302,宋方敏，南京大学 计算机科学与技术系, 江苏 南京 21002303

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

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

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