| 一种基于属性的操作系统内核自动验证方法 |
| |
| 引用本文： | 张琼声,吴明泉.一种基于属性的操作系统内核自动验证方法[J].小型微型计算机系统,2013,34(7). |
| |
| 作者姓名： | 张琼声 吴明泉 |
| |
| 作者单位： | 中国石油大学(华东)计算机与通信工程学院,山东青岛,266580 |
| |
| 基金项目： | 中央高校基本科研业务类专项资金 |
| |
| 摘 要： | 传统的模型检测摒除了很多软件实现细节,要检测实际的代码,就需要从代码中直接建立抽象描述.而操作系统内核结构复杂,手动对源代码进行抽象存在建模工作量大、人工参与过多易出错以及属性难以描述和检测等问题.本文以Linux内核作为实验对象,提出了一种基于属性的OS内核自动验证方法,利用模型抽取工具Modex自动的从inux内核源代码抽取模型,试图保证模型与实现代码一致性的同时减少因人工参与产生的人为错误,然后用时间轴属性来描述属性,最后用模型检测工具Spin对Linux内核代码模型进行检测.实验选取了Linux内核中接口和数据结构相对复杂的调度器进行模型的自动抽取与属性检测,验证了该方法在操作系统内核模型检测中的有效性和实用性.
|
| 关 键 词： | 操作系统 模型检测 Spin Modex |
Pragmatic Approach to Automated Verifying Operating System Based on Properties |
| |
| ZHANG Qiong-sheng
,
WU Ming-quan.Pragmatic Approach to Automated Verifying Operating System Based on Properties[J].Mini-micro Systems,2013,34(7). |
| |
| Authors: | ZHANG Qiong-sheng WU Ming-quan |
| |
| Abstract: | |
| |
| Keywords: | operating system model checking Spin Modex |
| 本文献已被 万方数据 等数据库收录！ |
|
