Nasa ams java path finder software#

In SPF, programs are executed on symbolic inputs representing multiple concrete inputs and the values of program variables are represented by expressions over those symbolic inputs.

Nasa ams java path finder software#

Although we give our presentation in the context of a NASA project, we believe that our work is relevant for other critical systems that require thorough testing.read more read lessĪbstract: Symbolic PathFinder (SPF) is a software analysis tool that combines symbolic execution with model checking for automated test case generation and error detection in Java bytecode programs. Our analysis helped discover a serious bug that resulted in design changes to the software.

We applied our approach to testing a prototype NASA flight software component. Furthermore, we use two techniques that leverage system-level concrete program executions to gather information about a unit's input to improve the precision of the unit-level test case generation. The framework propagates the symbolic information via attributes associated with the program data.

We have developed Symbolic Java PathFinder, a symbolic execution framework that implements a non-standard bytecode interpreter on top of the Java PathFinder model checking tool. Abstract: We describe an approach to testing complex safety critical software that combines unit-level symbolic execution and system-level concrete execution for generating test cases that satisfy user-specified testing criteria.