软件测试是为了发现错误而执行程序的过程,是保证软件质量的重要手段,因而成为软件生命周期中的重要阶段。在已有的测试工具中,源代码测试工具有着重要的应用。模型检查则是一种遍历系统所有可能执行路径的自动验证技术。最早由E.M.Clarke和E.A.Emerson在1981年提出,主要是米验证有穷状态并发系统的命题性质。它通常采用状态空间搜索的方法来检查一个给定的计算模型(程序)是否满足某个特定性质。在基于模型检查的软件代码分析和可靠性验证方面,国外少数大学和研究机构已经取得了一定的进展。目前仍需要解决和改善的问题主要集中在效率和准确性两个方面。　　 本文主要讨论和分析了程序模型建立、模型检查和模型精化等方面的研究现状。针对软件单元测试和系统整合测试等阶段遇到的程序接口调用问题,给出了一个具体的方案。本文提出了多种策略尽可能满足用户对效率和准确性方面的不同需求,同时详细探讨了基于模型检查的程序测试框架中各个阶段使用的技术和算法,并于最后描述了基于模型检查的程序接口调用分析测试系统的设计与具体实现。通过本文给出的程序测试系统,可以帮助软件开发人员和测试人员软件在接口调用等方面是否存在错误和缺陷,检测源程序是否会出现因为接口调用所引起的内存泄漏和系统安全漏洞等问题,进而提高软件的可靠性和质量。