10.3969/j.issn.1000-3428.2009.11.044
采用SPIN的L4内存管理形式化验证
模型检验通过状态空间搜索检验一个给定的计算模型是否满足某个用时序逻辑公式表示的特定性质.对L4微内核操作系统的内存管理机制进行形式化抽象建模,针对L4内核API提供的地址空间操作原语Grant,Map和Flush等操作进行形式化描述,模拟地址页面映射的树形结构管理,运用模型检验工具SPIN对抽象模型进行了验证.
L4微内核、地址空间操作原语、模型检验
35
TP309(计算技术、计算机技术)
国家自然科学基金资助项目60773170,60721002;国家"863"计划基金资助项目2006AA01ZA32
2009-07-10(万方平台首次上网日期,不代表论文的发表时间)
共3页
131-133