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

摘要：

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

关键词：操作系统、形式化设计、形式化验证、定理证明、系统安全、框架设计

所属期刊栏目：38

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

资助基金：国家"863"计划基金资助项目"分布式可信计算系统研究"2007AA012409;国家自然科学基金资助项目60721002;江苏省科技支撑计划基金资助项目"可信操作系统新技术研发"BE2008124

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

页数：共5页

页码：234-238