目前,随着开源软件数量的飞速增长,使用开源软件的用户群体越来越大,开源软件涉及到的应用领域也在不断扩大,随之而来的软件安全问题也颇为引人注目。在开源软件安全隐患层出不穷的时代,关于开源软件安全缺陷与漏洞检测的研究成为了软件测试领域的热点问题。本文的主要目的是找到一种开源软件安全缺陷与漏洞检测的自动化方法,扩大检测范围,提高检测效率。模型检测作为一种高效的形式化静态检测技术,能够直接基于源代码的角度,对软件中隐藏的缺陷与漏洞进行检测。模型检测技术既是一种自动化检测技术,在此基础上还可以保证检测的精度和正确性,因此其无论是在学术上还是在实践中都具有较高的价值。本文总结了目前使用广泛的开源软件检测方法及工具,并且分析了模型检测理论在开源软件检测方面的研究与应用情况,提出了一种基于模型检测的开源软件安全缺陷与漏洞检测方法。该方法基于近年新兴的条件模型检测理论,通过将两个以上的模型检测算法以串行方式运行的形式,降低模型检测器的失败概率,从而扩大可检测漏洞的范围;同时,本文在深度剖析模型检测工具CPAChecker的体系结构及核心算法的基础上,给出了可配置程序分析的形式化描述和算法流程,并且利用可配置程序框架实现条件模型检测算法的自动化执行,从而提高模型检测的效率。最后,对开源web服务器软件Tomcat执行条件模型检测,实验结果表明,在其他检测方法的基础上,条件模型检测能够发现其他检测无法发现的软件漏洞。