微内核架构内存管理的形式化设计和验证方法研究

• 作者: 刘永俊 姚宇峰 宋方敏 汤力 钱振江 黄皓
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 操作系统 内存管理 形式化设计 形式化验证 定理证明
• 年，卷（期）: 2017,（1）
• 所属期刊栏目: 科研通信
• 页码范围: 251-256
• 页数: 6页
• 分类号: TP316
• 字数: 6279字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2017.01.035

摘要

由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare 三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS(Verified Secure Operating System)内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄皓	南京大学计算机科学与技术系	140	1805	24.0	35.0
2	刘永俊	常熟理工学院计算机科学与工程学院	42	118	5.0	8.0
3	钱振江	南京大学计算机科学与技术系	16	90	6.0	8.0
7	宋方敏	南京大学计算机科学与技术系	29	191	9.0	13.0
8	姚宇峰	常熟理工学院计算机科学与工程学院	14	67	4.0	8.0
9	汤力	常熟理工学院计算机科学与工程学院	3	11	3.0	3.0