Research on Formal Specification-Based Program Testing

在本项目中，我们对基于形式化规范的程序测试的理论、方法和支持工具进行了深入的研究。结果，我们已经完成了3份期刊出版物，9份国际会议出版物，以及我们开发的测试方法的原型软件工具。我们的研究重点集中在以下几个方面。首先，我们提出了“功能场景”的概念作为检查程序中相应实现的基本标准，并提出了“功能场景形式(FSF)”的概念作为测试用例生成的最合适结构。我们已经提出了将任何后置条件样式规范自动转换为FSF的算法，以及用于生成适当测试用例的一组标准。其次，我们建立了一种通过生成测试用例来检查前置后置条件样式规范的方法。第三，我们开发了一个基于关系的测试用例生成器…更多的n方法。通过这种方法，可以根据程序输入变量之间的预定义关系自动生成测试用例。这种方法的优点是有效地将黑盒测试和白盒测试结合在一起，而不需要知道规范和程序的细节。第四，我们开发了一种集成了基于规范的检查技术和基于规范的测试技术的技术。该技术的总体思想是，首先基于其规范对程序进行严格的检查，以发现导致崩溃、无限循环或规范中定义的功能场景的不正确实现的程序错误，然后执行充分的基于规范的测试，以发现在程序执行期间发生的错误。第五，我们建立了一种测试程序的方法，测试人员无需源代码即可进行测试。这种方法强调使用程序的接口场景，可以通过使用简单的测试用例来检测，以形成前置条件和后置条件的形式规范。然后，该规范作为系统测试程序的基础，包括测试用例生成和测试结果分析。这种方法的意义在于，它可以有效地用于在公共领域中找到令人满意的组件，并执行系统和验收测试。最后，我们开发了一个原型软件工具来支持基于规格说明的测试技术。该工具帮助我们演示了上述基于规范的测试技术的工具可支持性。较少

In this project, we have conducted intensive research on the theory, methods, and supporting tool of program testing based on formal specifications. As the result, we have achieved three journal publications, nine international conference publications, and a prototype software tool for the testing method we have developed. The focus of our research is on the following aspects. Firstly, we have proposed the concept of “functional scenario" as the basic criterion for checking the corresponding implementation in the program, and the notion of “functional scenario form (FSF)" as the most suitable structure for test case generation. We have come up with an algorithm for automatically transforming any pre-post-condition style specification into an FSF, and a set of criteria for generating adequate test cases. Secondly, we have established a method for inspecting a pre-post-condition style specification via generating test cases. Thirdly, we have developed a relation-based test case generatio … More n method. By this method, test cases can be automatically generated based on pre-defined relations between input variables of a program. The advantage of this method is that it effectively combines the black-box and white-box testing, without the need to know the details of both the specification and the program. Fourthly, we have developed a technique that integrates the specification-based inspection technique and the specification-based testing techniques. The overall idea of the technique is that a rigorous inspection of the program based on its specification is first carried out to find program bugs that cause crashes, infinite loops, or incorrect implementation of the functional scenarios defined in the specification, and then a sufficient specification-based testing is performed to find bugs occurred during program executions. Fifthly, we have established an approach to testing programs without source code available to testers. This approach emphasizes the use of the interface scenarios of the program, which can be detected by using simple test cases, to form a formal specification in pre- and post-conditions. The specification then serves as the basis for a systematic testing of the program, including test case generation and test result analysis. The significance of this approach is that it can be effectively used to find satisfactory components in the public domain and to perform system and acceptance testing. Finally, we have developed a prototype software tool to support the specification-based testing techniques. The tool has helped us demonstrate the tool supportability of our specification-based testing techniques mentioned above. Less