Overview
The objective of the automated testing project is to perform automated generation of test inputs that obtain high coverage for flexible (user-definable) coverage metrics and to check properties of code during test case generation.
To this end, we have developed a tool (JPF-SE), that combines symbolic execution with model checking and constraint solving for test case generation. In this tool, programs are executed on symbolic inputs that cover all possible concrete inputs. Values of variables are represented as numeric constraints, generated from analysis of the code structure. These constraints are then solved to generate test inputs guaranteed to reach that part of code. JPF-SE uses the analysis engine of the Ames JPF model checking tool.
JPF-SE
- Applies to (executable) models and code
- Generates an optimized test suite that exercise all the behavior of the system under test
- Reports coverage
- During test generation process, checks for errors
- Is flexible, as it allows for easy encoding of different coverage criteria
- Integration with simulation environment
Applications
Test input generation for Java container classes, NASA guidance navigation and control (GNC) software, script generation for testing execution engines
