Study On The Automatic Class Test Generation Techniques With Model Check

The highly reliable software technique is one of the focuses in the software theorystudy and the software engineering practice. Recently, more and more formal methodshave been exploited for software quality study. The software testing is one of theeffective methods for assuring software reliability and accuracy, and the model check isan automatic formal verification method ensuring the correctness of specifications andcodes. Researches show that the counterexample in the model check is an effect applyingfor generating the test cases, and it can reduce notably the testing cost, and heighten thesoftware quality. This paper mainly studies the techniques for automatic generatingclass testes based model check.This paper introduces the data-flow testing and mutation testing into the modelchecker Java PathFinder(JPF), transforms the problem of test generation into the one offinding the counterexample in model check, and designs two methods to generateoriented-object software testing automatically.First, by applied trap properties and the temporal logic relationship, we design asearching algorithm to generate the test sequences automatically, and implement it withJPF. The algorithm satisfies the criterion of data-flow coverage and generates testes formethod calling in a Java class. The experimental results show that the presentedalgorithm enhances 8％coverage by the right search depth, and can find the hiddenfaults in the program, shorten the calling sequences length by the selection principles inthe methods calling. Compared with the DFS algorithm in JPF, the presented algorithmdrops the excess states yielded in the search process, and backtracks in time, in the caseof the same memory, the number of new states decrease 65％, backtracks numberreduce 90％, the processed states drop by 88％, and run times subtract 28％. Thepresented algorithm reduces remarkably the test generation cost.Second, based on the mutation test theory and class-duplication method, anautomatic generation approach of the test for inter-class is presented and implementedby applying the JPF to make the propagation of faults be the visible outputs. Thealgorithm analysis and experimental results show that the presented approach overlay the main object-oriented feature and yield 211 mutants for TreeMap class, we cover allthe valid mutants by 21 counterexamples, reduce the test generation cost remarkably.Compare with the Symbolic Execution method in JPF presented by Visser, the presentedapproach raise the coverage about 15％for deleteEntry, fixAfterDeletion andfixAfterlnsertion methods in TreeMap class, the valid coverage reach 100％. Further,our approach does not depend on the design of program structure, and make thepropagation of faults be the visible outputs to finding the hidden errors.