操作系统的正确性是计算机系统可靠性、安全性以及计算机系统提供可信计算的重要基础,但是由于操作系统内核复杂、规模庞大,目前的软件正确性验证技术在发现操作系统错误方面能力有限。基于模型的软件测试技术往往能发现其它测试技术难以发现的软件错误,具有测试效率高的优点。近年来,模型检测技术应用于操作系统的正确性验证虽然已经取得了重要的突破。但是在对内核复杂模块进行模型检测、状态爆炸、寻求资源耗费与检测覆盖的平衡等方面还存在有待解决的诸多问题。本文以Linux操作系统内核为实验对象,对Linux内核调度器及其外部环境建立Promela模型,在模型检测工具Spin中实现调度器代码级错误检测。研究结果表明,文中提出的模型系统有效地解决了针对具有复杂接口的操作系统内核模块建立检测模型的问题。本文根据实验过程和结果,提出了一种用Promela描述的外围环境模型来驱动调度器模型工作的方法。此外针对建立Promela调度器模型面临的复杂C语言代码转化为Promela语言存在的问题提出了有效的解决方法,对解决类似问题具有参考价值。