随着计算机产业的快速发展,软件的规模不断扩大,软件的测试工作也越来越复杂,如何提高测试的效率已成为被广泛关注的问题。形式化方法的研究和应用已有30多年的历史,它的优越之处在于它有严格的数学基础和描述的精确性,在软件的开发和测试过程中能够准确描述系统,并减少由误解引起的错误。本文基于形式化的软件描述方法,针对开发流程的测试阶段,研究了如何提供一种自动化或者半自动化的安全测试方法,检测程序中存在的安全漏洞。本文借助现有的Z规格描述方法和黑盒测试方法,提出一种基于形式化的软件测试方法。首先,获取用户的UML时序图,确定用户的系统中哪些执行过程可能存在安全漏洞;并进一步获取用户对系统的Z规格描述,并对此Z规格进行初步的分析。其次,利用Z规格的分析结果自动或者半自动地生成测试用例,并对测试用例进行进一步的简化。最后,获取用户的真实工程代码,将测试用例输入代码当中,完成对代码的测试,找到软件中存在的漏洞和缺陷。在此之上,本文设计并实现了一个安全测试工具,功能模块包括Z规格分析模块,测试用例生成模块和测试执行模块。该工具的开发基于Eclipse,并可被进一步集成到其他软件开发环境中。该测试方法给测试人员提供了相对自动化的工具支持,降低了测试工作对测试人员的技术与经验的依赖,减少了人工参与的成分,提高了测试用例的有效性。其可以作为安全软件开发环境中的一部分,为构建安全可靠的软件起到了很好的作用。