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

作者：陈超超; 曾庆凯

来源：计算机工程, 2009, (11): 131-133.

• L4微内核
• 地址空间操作原语
• 模型检验 L4 microkernel
• address space primitives
• model check

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