应用于操作系统内核正确性验证的模型检测技术的研究

摘要

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

目录

文摘

英文文摘

声明

第一章前言

第二章模型检测技术

2.1模型检测技术的基本概念及算法

2.1.1模型检测基本思想

2.1.2 Kripke模型

2.1.3模态／时序逻辑

2.1.4模型检测算法及其时空效率

2.2模型检测技术的发展及现状

2.3应用于软件正确性分析的模型检测技术

2.4模型检测相关工具介绍

2.4.1应用于硬件和协议验证的模型检测工具

2.4.2应用于软件的模型验证工具

第三章应用于操作系统正确性分析的模型检测

3.1应用于操作系统正确性分析的模型检测技术的发展现状

3.2模型检测应用于操作系统正确性分析方法概述

3.2.1模型检测应用于TCP/IP协议及文件系统

3.2.2模型检测应用于设备驱动程序

3.2.3模型检测应用于Linux内核的部分安全属性的验证

3.2.4模型检测技术与操作系统内核设计结合

3.3模型检测技术在操作系统内核正确性验证中面临的问题

第四章模型检测Linux内核调度器

4.1 spin和promela简介

4.1.1模型检测工具Spin

4.1.2建摸语言promela

4.2 Linux2.6.11的进程调度器

4.2.1 Linux2.6.11的进程调度器

4.2.2 Linux2.6.11的进程调度器外部环境

4.3调度器的promeIa模型

4.3.1 Linux2.6.11调度器promela模型的构成

4.3.2调度器模型建立面临的问题及解决方法

4.3.3建立调度器Promela模型的步骤

4.4调度器外围环境的模型化

4.4.1调度器外围环境模型的构成

4.4.2调度器外围环境模型的建模

4.4.3调度器外围环境步骤

4.4.4调度器外围环境驱动调度器情景分析

4.5验证

4.6相关工作比较

4.7本章小结

第五章总结

5.1本文工作总结

5.2下一步研究方向

参考文献

攻读硕士学位期间取得的学术成果

致谢