基于Z规格的软件测试工具的设计与实现

摘要

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