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

摘要：

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

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

所属期刊栏目：27

分类号：TP316(计算技术、计算机技术)

资助基金：国家自然科学基金61402057;江苏省科技计划自然科学研究项目BK20140418;中国博士后科学基金2015M571737;江苏省“六大人才高峰”高层次人才项目2011-DZXX-035;江苏省高校自然科学研究项目12KJB520001National Natural Science Foundation of China61402057;the Natural Science Foundation of Jiangsu ProvinceBK20140418;China Postdoctoral Science Foundation2015M571737;the "Six Talents Peak" High-Level Personnel Project of Jiangsu Province2011-DZXX-035;Natural Science Foundation of the Higher Education Institutions of Jiangsu Province of China12KJB520001

在线出版日期：2017-01-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共15页

页码：3143-3157