The Application Testing And Verification Based On Symbolic PathFinder

The development of software testing has drawn more and more attention withthe demands of the reliability and safety of the software is rising, so the modelchecking is an automatic formal verification method, in order to ensure thecorrectness of a system design’s specifications.JPF is a tool of an explicit state model checker for testing Java bytecode, it is aspecial Java Virtual machine that execute a program not just once, but in the theory inall possible ways. JPF helps checking the concurrent programs in the multi-threads,where there are some potential errors such as deadlock and unhandled exception. JPFprovides several extension points, like Choice generator, Instruction factory, AttributeSystem、 the Model Java Interface, Listeners and Reporter. Symbolic PathFinder(SPF) is a software analysis tool that combines symbolic execution with modelchecking for automated test case generation and error detection in Java bytecodeprograms.SPF is an extension project in JPF. In Symbolic PathFinder, programs areexecuted on symbolic inputs instead of multiple concrete inputs and the values ofprogram variables are represented by expression over those symbolic inputs.Constraints over these expressions are generated from the analysis of different pathsthrough the program. The constraints are solved with off-the-shell solvers todetermine path feasibility and to generate test inputs. SPF is tightly integrated withthe JPF model checker，JPF framework provides SPF the ability to systematicallyexplore symbolic program paths, different thread interleavings, and other forms ofnon-determinism present in the code.Based on the study of the software model checking of SPF, implementationmechanism of running Java bytecode, strengthen the functional analysis of the systemstate of SPF in order to find the new errors in the system. We also have highlightedsome of the techniques that are built into SPF to handle complex mathematicalconstraints, external library calls and symbolic string analysis. To verification SPFcan effectively solve the path cover problem in circulation and recursive programs we described several applications on the Eclipse platform, as well as perform higher codecoverage in SPF symbolic execution than concrete execution.