Software Verification and Validation (VIMMD052)
Code-based test generation
Dávid Honfi, Zoltán Micskei, István Majzik
Budapest University of Technology and Economics
Dept. of Artificial Intelligence and Systems Engineering
Budapest University of Technology and Economics
Dept. of Artificial Intelligence and Systems Engineering 1
Where are we now in the development process?
Requirement
analysis
System
specification
Architecture
design
Component
design
Component
implementation • Source code analysis
• Proof of program correctness by theorem proving
System • Software model checking with abstraction-based methods
integration
• Component testing: classic techniques
System • Component testing: code-based testing
delivery
Operation,
maintenance
2
Motivation
Goal: Developer testing of software components
(modules, units)
o At this level, detailed specification may be missing
Idea: Generate test inputs based on the source code
o Execute all parts of the code
(this way source code coverage criteria can be satisfied)
How test outputs are checked?
o Based on overall expectations (derived from higher level
specifications)
o Using generic criteria: avoiding crash, OS level error signal,
exception, timeout, violated assertion
o Re-using outputs of previous test (regression testing)
3
1. Random test generation
Random selection of input data from the input domain
Advantage:
o Very fast
o Very cheap
Ideas:
o If no error found: trying different parts of the input domain
o Selection based on ”difference”, ”distance” of values
Example tool for Java: Randoop
8
Random test generation: The Randoop tool
Generation a sequence of method calls
Creating object parameters using random values in
the constructor
Heuristics:
o Execution of the selected test case
o Throwing away random tests that seem to be redundant
o Using invalid values for robustness testing
9
2. Annotation-based test generation
The code shall contain:
o Pre- and post-conditions (e.g.: design by contract)
o Other annotations (e.g., loop invariants)
These are able to guide test generation
o Preconditions: to be satisfied
(or violated if robustness is tested)
o Postconditions, invariants: to be checked
/*@ requires amt > 0 && amt <= acc.bal;
@ assignable acc.bal;
@ ensures acc.bal == \old(acc.bal) - amt;
@*/
public void transfer(int amt, Account acc) {
acc.withdraw(amt);
deposit(amt);
}
12
Annotation-based test generation: Example tools
AutoTest
o For the Eiffel language, with design by contract
o Input: object pool
• Random generation of inputs that satisfy the preconditions
o Expected output: checked on the base of the contracts
o Ref: Bertrand Meyer et al., "Program that Test Themselves", IEEE Computer
42:9, 2009.
QuickCheck: Property based test generation
o Goal: Generate test values that take into account the types
and constraints of the input domains
o Ref: Claessen et al. "QuickCheck: a lightweight tool for random testing of
Haskell programs“ ACM Sigplan 46.4 (2011): 53-64
13
3. Search-based techniques
Approach: Search-based Software Engineering (SBSE)
Representing a problem as a search:
o Search space:
Possible test inputs + structure of the tested program
o Objective function: reaching a test goal
• Coverage criteria: statements, decision branches
• Minimization of the size of the test suite
Using metaheuristic algorithms
o Genetic algorithms: a random initial test set and
mutations or crossover + the objective function
• Mutations: Changes in test inputs, adding / removing calls
• Crossover: Combining existing test cases to generate a new set
• Keeping the new test cases that increase the objective function
16
Search-based techniques: Mutation and crossover
Crossover on test cases
Mutations on test cases
Crossover on test suites
17
Search-based techniques: The EVOSUITE tool
„Whole test suite generation”
o All test goals are taken into account
o Searches are based on multiple metrics: coverage and test suite size
o Uses sandbox for environment interaction
Example: Increasing coverage vs different search algorithms:
18
4. Symbolic execution
Static program analysis technique
Basic idea:
o Following the computation of program paths on the
basis of the source code, with symbolic variables
o Deriving reachability conditions as path constraints (PC)
o Constraint solving on path constraints (e.g., using an
SMT solver):
A solution provides inputs to execute the given path
Popular nowadays:
o Efficient SMT solvers exist
o Used to generate test inputs for covering given paths
20
Symbolic execution: Program paths and related inputs
int fun1(int a, int b){ Exploring program paths,
if (a == 0){ identifying branch conditions
1 printf(ERROR_MSG); Deriving path constraint (PC)
2 return -1; for each path
}
if (b > a)
a == 0
3 return b*a + 5; F T
else
4 return (a+b) / 2; a: 0
b > a b: 0
}
F T
PC for this path:
(a==0) (b>a) a: 2 a: 1
b: 1 b: 2
Selecting inputs that satisfy PC
22
Symbolic execution: Path constraints in a symbolic way
Path constraint Statement ID
Symbolic variables x, y
initial values X, Y
23
Symbolic execution: Example tools
Name Platform Language Notes
KLEE Linux C (LLVM bitcode)
IntelliTest Windows .NET assembly Formerly: Pex
SAGE Windows x86 binary Security testing
Jalangi - JavaScript
Symbolic - Java
PathFinder
Other (mainly discontinued) tools:
CATG, CREST, CUTE, Euclide, EXE, jCUTE, jFuzz, LCT, Palus, PET, etc.
More tools: http://mit.bme.hu/~micskeiz/pages/cbtg.html
27
Symbolic execution: Microsoft IntelliTest
Generate unit tests for your code with IntelliTest
https://learn.microsoft.com/en-us/visualstudio/test/generate-
unit-tests-for-your-code-with-intellitest
Input variable: ”condition”
Test inputs generated Test outputs SEViz (Symbolic Execution Visualizer)
for variable ”condition” (incl. exception here) https://github.com/FTSRG/seviz
28
Symbolic execution: Challenges for symbolic execution
1. Huge number of execution paths
2. Complex arithmetic expressions
3. Floating point operations
4. Compound structures and objects
5. Pointer operations
6. Interaction with the environment
7. Multithreading
8. …
T. Chen et al. „State of the art: Dynamic symbolic execution for automated test generation”.
Future Generation Computer Systems, 29(7), 2013
32
Symbolic execution: Challenge 1
Huge number of execution paths
int hardToTest(int x){
for (int i=0; i<100; i++){
int j = complexMathCalc(i,x);
if (j > 0) break;
}
return i;
}
Solution ideas:
o Various loop traversal algorithms (instead of DFS)
o “Method summary”: simple representation of methods
33
Symbolic execution: Challenge 2
Complex arithmetic expressions
Most SMT solvers cannot handle these
int hardToTest2(int x){
if (log(x) > 10)
return x
else
return -x;
}
Ideas: Using specific solvers
34
Symbolic execution: Challenge 6
Interaction with the environment
Calls to platform and external libraries
int hardToTest3(string s){
FileStream fs = File.Open(s, FileMode.Open);
if (fs.Lenth > 1024){
return 1;
} else
return 0;
}
}
Idea:
o „Environment models” (KLEE): for simple C programs
o Special objects representing the environment (Java)
36
Evaluation: Applying code-based techniques
A large-scale embedded system (C)
o Execution of CREST and KLEE on a project of the company ABB
o ~60% branch coverage reached
o Fails and issues in several cases
X. Qu, B. Robinson: A Case Study of Concolic Testing Tools and Their Limitations, ESEM 2011
Does it help software developers?
o 49 participants wrote tests and also generated tests
o Generated tests with high code coverage did not discover
more injected failures than manual tests
G. Fraser et al., “Does Automated White-Box Test Generation Really Help Software Testers?,” ISSTA 2013
Finding real faults
o Defects4J: database of 357 issues from 5 projects
o Tools evaluated: EvoSuite, Randoop, Agitar
o Found 55% of faults – problem: requirements were missing
S. Shamshiri et al., „Do automatically generated unit tests find real faults? An empirical study of effectiveness
and challenges.” ASE 2015
38
