| 采用SPIN的L4内存管理形式化验证 |
| |
| 引用本文： | 陈超超,曾庆凯.采用SPIN的L4内存管理形式化验证[J].计算机工程,2009,35(11):131-133. |
| |
| 作者姓名： | 陈超超 曾庆凯 |
| |
| 作者单位： | 1. 南京大学计算机软件新技术国家重点实验室,南京,210093
2. 南京大学计算机科学与技术系,南京,210093 |
| |
| 基金项目： | 国家自然科学基金，国家高技术研究发展计划(863计划) |
| |
| 摘 要： | 模型检验通过状态空间搜索检验一个给定的计算模型是否满足某个用时序逻辑公式表示的特定性质。对L4微内核操作系统的内存管理机制进行形式化抽象建模，针对L4内核API提供的地址空间操作原语Grant，Map和Flush等操作进行形式化描述，模拟地址页面映射的树形结构管理，运用模型检验工具SPIN对抽象模型进行了验证。
|
| 关 键 词： | L4微内核 地址空间操作原语 模型检验 |
| 修稿时间： | |
Formal Verification of L4 Memory Management Using SPIN |
| |
| CHEN Chao-chao,ZENG Qing-kai.Formal Verification of L4 Memory Management Using SPIN[J].Computer Engineering,2009,35(11):131-133. |
| |
| Authors: | CHEN Chao-chao ZENG Qing-kai |
| |
| Affiliation: | 1.Key Laboratory for Novel Software Technology;Nanjing University;Nanjing 210093;2.Department of Computer Science and Technology;Nanjing 210093 |
| |
| Abstract: | |
| |
| Keywords: | L4 microkernel address space primitives model check |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载全文 |
