VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究

• 作者: 宋方敏 钱振江 黄皓
• 来源期刊: 南京大学学报（自然科学版）
• 学科: 工学
• 关键词: 操作系统 内核硬件抽象模型 形式化验证 Isabelle/HOL 定理证明
• 年，卷（期）: 2017,（3）
• 所属期刊栏目: 硅基纳电子和光电子专栏
• 页码范围: 579-589
• 页数: 11页
• 分类号: TP316
• 字数: 8041字
• 语种: 中文
• DOI: 10.13232/j.cnki.jnju.2017.03.022

摘要

形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如何有效地对汇编语言代码进行建模,便于对其语义和功效的正确性进行验证成为操作系统形式化领域的研究热点.在汇编级提出对操作系统的设计和实现的正确性进行形式化验证的方法.通过建立操作系统内核硬件抽象模型,形式化地描述指令的操作语义,在此内核硬件抽象模型的基础上界定影响系统状态变化的数据对象,建立系统状态空间,结合指令的操作语义的定义来描述系统的状态转换函数.在Isabelle/HOL定理证明器环境中描述该内核硬件抽象模型,以实现的可信操作系统VSOS为例,在汇编级对系统设计和实现的正确性进行验证.结果表明,该方法是可行的和高效的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄皓	南京大学软件新技术国家重点实验室	140	1805	24.0	35.0
2	钱振江	常熟理工学院计算机科学与工程学院	16	90	6.0	8.0
6	宋方敏	南京大学软件新技术国家重点实验室	29	191	9.0	13.0