操作系统是计算机系统中最基本、最重要的软件,其安全性和可靠性是计算机系统提供可信计算的首要条件,也是其它应用软件正常运行的基本保障。但是操作系统内核结构复杂、规模庞大,其开发与调试都十分困难,一些隐藏的错误用一般的软件测试及验证技术很难发现。模型检测技术具有简洁明了、自动化程度高等特点,往往能发现其他测试技术难以发现的软件错误,传统的模型检测摒除了很多软件实现细节,要检测实际的代码,就需要从代码中直接建立抽象描述。而操作系统内核结构复杂,手动对源代码进行抽象存在建模工作量大、人工参与过多、易出错以及属性难以描述和检测等问题。　　 本文以Linux内核作为实验对象,提出了一种基于属性的操作系统内核自动验证方法,利用模型抽取工具Modex从Linux内核源代码自动抽取模型,试图保证模型与实现代码一致性的同时减少因人工参与产生的人为错误,然后用时间轴属性来描述源代码应有的属性,最后用模型检测工具Spin对Linux内核代码模型进行检测。实验选取了Linux内核中接口和数据结构相对复杂的调度器进行模型的自动抽取与属性检测,验证了该方法在操作系统内核模型检测中的有效性和实用性。