摘要： 模型检验通过状态空间搜索检验一个给定的计算模型是否满足某个用时序逻辑公式表示的特定性质。对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

中图分类号: 

• TP309