计算机工程 ›› 2009, Vol. 35 ›› Issue (11): 131-133.doi: 10.3969/j.issn.1000-3428.2009.11.044

• 安全技术 • 上一篇    下一篇

采用SPIN的L4内存管理形式化验证

陈超超,曾庆凯   

  1. (1. 南京大学计算机软件新技术国家重点实验室,南京 210093; 2. 南京大学计算机科学与技术系,南京 210093)
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2009-06-05 发布日期:2009-06-05

Formal Verification of L4 Memory Management Using SPIN

CHEN Chao-chao, ZENG Qing-kai   

  1. (1. Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093; 2. Department of Computer Science and Technology, Nanjing University, Nanjing 210093)
  • Received:1900-01-01 Revised:1900-01-01 Online:2009-06-05 Published:2009-06-05

摘要: 模型检验通过状态空间搜索检验一个给定的计算模型是否满足某个用时序逻辑公式表示的特定性质。对L4微内核操作系统的内存管理机制进行形式化抽象建模,针对L4内核API提供的地址空间操作原语Grant, Map和Flush等操作进行形式化描述,模拟地址页面映射的树形结构管理,运用模型检验工具SPIN对抽象模型进行了验证。

关键词: L4微内核, 地址空间操作原语, 模型检验

Abstract: Model checking is a technique that relies on building a finite model of the system and checks whether the desired properties hold in that model. The check is performed as an exhaustive state space search. This paper introduces a model for L4 microkernel memory management system, gives formal description for operations such as Grant, Map, Flush, proposes and verifies some safety properties using SPIN model checker.

Key words: L4 microkernel, address space primitives, model check

中图分类号: