本文旨在研究软件模型检测及其工具实现，包括模型的表示、检测的算法、实现方案、案例分析和如何与软件开发过程相结合等问题。本文从模型检测、软件模型检测的基本理论讲起，深入论述了软件模型检测的重要技术，系统地介绍了数个对当前软件模型检测影响比较大的检测工具及其技术。 　　在总结前人的成果后，本文提出了基于CERL语言的表达方法，提出了用CERL作为中间层的转化式模型检测方案并以从CERL到SMV的转化为例子总结了该方案的主要问题并给出相应解决策略，提出基于路径谓词的检测方案、算法并给出优化方法。作者在系统分析SMV模型检测工具的基础上实现了自己的方案，这里我们实现如何用SMV语言来模拟CERL语义的算法并把转化式方案和基于路径的检测方案有机统一起来。在讨论如何使软件模型检测和实际软件开发相结合的问题时候，我们引入了使用断言机制的方法。 　　在实验方面，本文对三个比较有代表性的程序作了分析，说明本文工具的实用性。最后本文对自己的方案的进一步完善和研究进行了简单探讨。