Linux内核调度器的模型检测

摘要

模型检测技术应用于操作系统中具有复杂接口的模块还存在检测模型难以建立的问题。本文提出了一种Linux内核调度器的模型系统，包括以Linux内核调度器触发条件为基础构建的调度器外围环境模型，和将Linux调度器C源代码直接转化为Promela描述的调度器模型。实验中构建了Linux2．6．11进程调度器的检测模型，并在Spin中实现了对模型系统的模拟仿真和错误检测。结果表明，文中提出的模型系统有效地解决了针对具有复杂接口的操作系统内核模块建立检测模型的问题。