操作系统形式化设计与验证综述

• 作者: 刘苇 钱振江 黄皓
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 操作系统 形式化设计 形式化验证 定理证明 系统安全 框架设计
• 年，卷（期）: 2012,（11）
• 所属期刊栏目: 开发研究与设计技术
• 页码范围: 234-238
• 分类号: TP316
• 字数: 5859字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2012.11.072

摘要

对操作系统的形式化设计和验证的概念进行介绍,描述其框架和基本方法.比较和分析操作系统宏内核和微内核结构,调查多个设计和验证项目,阐述项目的验证目标、方法、优缺点和进展情况.在总结研究现状的基础上,分析和展望操作系统形式化设计和验证的发展趋势,从操作系统模型设计、验证工具、代码实现和验证重用等方面给出形式化设计和验证的思路.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄皓	南京大学软件新技术国家重点实验室	140	1805	24.0	35.0
5	钱振江	南京大学软件新技术国家重点实验室	16	90	6.0	8.0
9	刘苇	南京大学软件新技术国家重点实验室	3	36	3.0	3.0