基于形式化规格说明的程序测试方法和工具的研究

摘要

软件测试和形式化方法是保证软件系统可靠性的两种方法。由于形式化方法研究在工程应用领域并没有取得突破性的研究成果，完全使用形式化方法不能解决现有的软件问题。而软件测试的方法和过程不是完全形式化的，必然包含一些规则、经验等非形式化的内容。因此，将形式化方法引入软件测试中，一方面实现了形式化方法在工程中的应用，另一个方面可以改善现有的测试方法，实现软件测试的自动化。 本文在形式化方法SOFL的基础上，提出了一个基于SOFL形式化规格说明的测试模型，重点研究测试用例的生成，逻辑覆盖准则和评估。这个模型描述为：首先确定程序中被测类与形式化规格说明的对应关系，从类的形式化规格说明导出类的状态转换图。然后把状态转换图看作有限自动机，就可以得到生成测试数据的方法，根据方法调用序列覆盖标准，就可以验证测试的完整性和一致性。最后根据逻辑覆盖的评估准则，分析测试的效果。 在这个测试模型基础上，实现了一个基于SOFL形式化规格说明的Java程序测试工具。这个工具首先确定SOFL形式化规格说明的Java程序的对应关系，然后根据形式化规格说明和选定的测试策略，辅助生成测试用例和并对结果进行分析。