Research on Formal Specification-Based Program Testing

点击翻译按钮获取中文摘要

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