随着信息技术的迅速发展，软件已经广泛应用于政治、经济、科技、国防和医疗等社会各个行业，软件中的任何安全漏洞都可能导致非常严重的后果。解决软件安全问题的根本在于软件交付运行之前成功消除所有潜在的安全漏洞，提高软件质量。因此，研究如何有效分析和验证软件，找出软件安全漏洞，成为信息安全领域的一个重要研究课题。本文主要针对软件分析技术中的模型检测技术进行研究和实现：　　 (1)对模型检测技术进行研究和分类。本文根据模型检测分析对象的不同，将模型检测分为三种类型：源码层次的模型检测、目标码层次的模型检测、以及可兼容处理两种层次代码的模型检测。在此分类的基础上，深入分析各类模型检测的具体实现技术，并对相应的代表性工具进行介绍。　　 (2)在模型检测工具MOPS的基础上，提出了数据流和控制流相结合的分析方法。MOPS具有很好的可扩展性，但由于采用控制流敏感、而数据流不敏感的分析方法，导致其分析精度的降低。本文通过引入指针别名数据流分析技术，使得MOPS在模型检测过程中同时考虑数据流和控制流信息，提高了分析精度。同时，为进一步降低误报率，实现了基于BLAST的反例路径验证技术。　　 (3)实现了高效的数据流分析方法。首先，提出了在安全漏洞模型指导下的程序切片方法。通过在模型检测之前依据构建的安全漏洞模型对程序进行切片预处理，得到程序中所有安全相关函数集合后再进行数据流分析等工作，保证了模型检测过程的简洁性和高效性，避免了巨大的时空开销。接着，提出了基于按需驱动的别名数据流分析改进方法。改进后的别名分析算法可以在程序切片基础上实现高效的按需驱动别名分析。　　 (4)基于提出的改进思想实现了相应的模型检测工具。该工具实现了数据流和控制流相结合的分析方法以及反例路径验证方法。实验结果表明改进后的模型检测工具能在较少时间开销的情况下，准确地分析出测试程序中存在的已知漏洞。