| 操作系统形式化设计与验证综述 |
| |
| 引用本文： | 钱振江,刘苇,黄皓.操作系统形式化设计与验证综述[J].计算机工程,2012,38(11):234-238. |
| |
| 作者姓名： | 钱振江 刘苇 黄皓 |
| |
| 作者单位： | 南京大学软件新技术国家重点实验室,南京210046;南京大学计算机科学与技术系,南京210046 |
| |
| 基金项目： | 国家"863"计划基金资助项目，国家自然科学基金资助项目，江苏省科技支撑计划基金资助项目 |
| |
| 摘 要： | 对操作系统的形式化设计和验证的概念进行介绍，描述其框架和基本方法。比较和分析操作系统宏内核和微内核结构，调查多个设计和验证项目，阐述项目的验证目标、方法、优缺点和进展情况。在总结研究现状的基础上，分析和展望操作系统形式化设计和验证的发展趋势，从操作系统模型设计、验证工具、代码实现和验证重用等方面给出形式化设计和验证的思路。
|
| 关 键 词： | 操作系统 形式化设计 形式化验证 定理证明 系统安全 框架设计 |
| 收稿时间： | 2011-10-15 |
Survey of Formal Design and Verification for Operating System |
| |
| QIAN Zhen-jiang
,
LIU Wei
,
HUANG Hao.Survey of Formal Design and Verification for Operating System[J].Computer Engineering,2012,38(11):234-238. |
| |
| Authors: | QIAN Zhen-jiang LIU Wei HUANG Hao |
| |
| Affiliation: | a,b(a.State Key Laboratory for Novel Software Technology;b.Department of Computer Science and Technology,Nanjing University,Nanjing 210046,China) |
| |
| Abstract: | This paper introduces the concepts of formal design and verification for the Operating System(OS),and elaborates the framework and foundational methods of formal design and verification.It compares and analyzes the monolithic kernel and micro kernel architectures of the OS.Meanwhile,it investigates multiple design and verification projects in depth,focusing on the verification objectives,the methodology,the advantages and limitations,and the progression.It summarizes the state of the art,analyzes and outlooks the trends of the formal design and verification for the OS.What is more,from the aspects of model design,verification tools,code implementation and verification reuse,it advances the ideas of formal design and verification. |
| |
| Keywords: | Operating System(OS) formal design formal verification theorem proving system security architecture design |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载全文 |
