一种基于属性的操作系统内核自动验证方法

Pragmatic Approach to Automated Verifying Operating System Based on Properties

传统的模型检测摒除了很多软件实现细节,要检测实际的代码,就需要从代码中直接建立抽象描述.而操作系统内核结构复杂,手动对源代码进行抽象存在建模工作量大、人工参与过多易出错以及属性难以描述和检测等问题.本文以Linux内核作为实验对象,提出了一种基于属性的OS内核自动验证方法,利用模型抽取工具Modex自动的从Linux内核源代码抽取模型,试图保证模型与实现代码一致性的同时减少因人工参与产生的人为错误,然后用时间轴属性来描述属性,最后用模型检测工具Spin对Linux内核代码模型进行检测.实验选取了Linux内核中接口和数据结构相对复杂的调度器进行模型的自动抽取与属性检测,验证了该方法在操作系统内核模型检测中的有效性和实用性.

Many software implementation details are discarded in the traditional model checking.Building abstract description from source code is needed if you check the real code.Because of the complexity of operating system,there are many problems to abstract source code manually： such as too much w orkload,human errors and difficulties in property description and checking.In this paper the Linux kernel is made as the experimental subject,and a pragmatic approach to automated verifying OS kernel based on properties is proposed.First use Modex to extract the model from Linux kernel code to guarantee the accordance of the model and implementation code w hile reducing human errors because manual w orkload.Then descript properties w ith time line.Last,use Spin to model checking Linux kernel code model.In the experiment,the scheduler is chosen to automatically extract model and property checking.The implement results show that this approach is effective and pragmatic in model checking OS kernel.