Research on Formal Specification-Based Program Testing

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

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