Minix操作系统是运行在PC机上的多用户、多任务的类Unix操作系统。Minix3是一款新的开源微内核操作系统,它松散的基于以前的Minix版本,它将大部分实现操作系统功能的服务移出了内核,内核代码数比以前的Minix版本更小,同其它体系结构的操作系统相比,具有高可靠性,高安全性以及易于扩展的优点。Minix系统基于模块化和分层设计,这种结构使得我们在将整个文件系统替换成别的不同的文件系统时变得更加容易,而无须重新编译内核。基于属性的测试技术关注程序中易于选定的待测属性进行测试,可以只针对一个或几个属性做测试,因此能减少测试量与增加测试效率,同时,在待测的属性中我们还可以加入系统中经常出现的错误,这样就增加了测试结果的可靠性。本文针对基于属性的Minix3操作系统的分析与测试生成工作展开,主要研究工作包括以下几个方面：首先,我们分析了微内核操作系统的特点,Minix3的体系结构以及Minix操作系统在结构上的改进,详细阅读了Minix3.1.1的源代码,深入分析了代码所实现的功能。其次,针对Minix3操作系统对属性做出了定义。对Minix3操作系统的28个内核调用建立了基于属性的Petri网模型,并对其模型进行了进一步的抽象,画出了Minix3内核实现的一些功能模型。再次,我们研究了程序切片和属性建模的关系,从中找出了一种基于程序切片和属性建模相结合方法来进行测试生成的途径,并设计了基于这种测试方法的测试生成系统。给出了程序切片技术在软件复用中的应用方法。最后,我们对Minix3操作系统一些重要的程序分别做了白盒测试、黑盒测试和基于属性的测试,并给出了测试结果。同时,我们对基于属性的测试的属性库进行了总结与归纳。下一步的研究重点是：为了减少软件模型复杂度,我们会考虑切片的粒度以及其它高层抽象的建模方法,并制定其抽象层次的标准。在以后的工作中,我们还将对属性进行形式化定义,并研究基于属性进行测试的测试覆盖的研究,以使得我们更加高效高质地对系统进行分析和测试。