Transcript Automated Test Generation

Korat: Automated Testing Based on
Java Predicates
Presented by : Praveen Kumar Vanga
Authors : Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko
Marinov
What is Korat ?




Korat, a framework for automated testing of
Java programs
Korat uses the method precondition to
automatically generate all test cases
Korat then executes the method on each test
case
Uses the method postcondition as a test output
to check the correctness of each output.
Motivations
Testing a Program Generated at Google.
 Input: Based on Acyclic Directed Graph (DAG)
 Strongly connected components of web graph
 Example of Structurally Complex input
- Structural : Data Consists of Linked Lists
- Complex : Nodes need to satisfy Properties
 Output : Set of Nodes on Certain Path


How to generate Such Test Inputs ?
Examples of Structurally Complex Data
red-black tree
1
0
3
2
XML document
<library>
<book year=2001>
<title>T1</title>
<author>A1</author>
</book>
<book year=2002>
<title>T2</title>
<author>A2</author>
</book>
<book year=2003>
<title>T3</title>
<author>A3</author>
</book>
</library>
/library/book[@year<2003]/title
Applications with Structurally Complex
Inputs
Operations on Abstract Data Types
- Input : Data structures Satisfying Invariants
Code Processing Java (IDE)
- Input : Correct Java Program (Syntactically and
Semantically)
XML Processing Systems
- Input : XML Documents
Many More.....
Testing Setup
inputs
outputs
1
0
2
3
0
2
test
generator
3
testing
oracle
code
3
2
0

3
0
pass
fail
Assumptions :
- User has knowledge about the Input of the code under test
- Knows the properties of desired Inputs

Large Number of Desired Inputs
- Ex: Corner cases for Linked List : empty LL, Non connected
List, disconnected LL, Linked List with Cycles...etc
Testing Setup
inputs
outputs
1
0
2
3
0
2
test
generator
3
testing
oracle
code
3
2
0

3
examples of code under test

abstract data type


input/output: data structure
XML processing program

input/output: XML document
0
pass
fail
Manual Test Generation
inputs
outputs
1
0
2
3
0
2
test
generator
• manual
testing
oracle
code
3
2
0

3
3
0
pass
fail
drawbacks of manual generation



labor-intensive and expensive
Tester Manually writes test abstractions and each test
abstraction describes a set of inputs
User might forget certain kind of test cases which
represent certain Inputs (Vulnerability)
Automated Test Generation
inputs
outputs
1
0
2
3
0
2
test
generator
• automated
testing
oracle
code
3
2
0

3
3
0
Tool Automatically Generates the inputs
- If test abstraction changes, tool regenerates Inputs

challenges of automated test generation
 describing test inputs
 (efficient) test generation
 checking output
pass
fail
Test Abstractions

Imperative : Describe how to generate Inputs
- ASTGen (More recent work - Discuss Later)

Declarative : Describe what Input looks like


Two Kinds of Languages used
Declarative Language for properties of desired
inputs (NLP)
- Properties written in Alloy Modeling Language
- Uses Alloy Analyzer for Generation of test cases

Imperative Language for Properties of Desired
Inputs
- Properties written in high-level languages (Java,
C#,...)
UseCase : Bounded-Exhaustive
Generation
Generate all valid Structures up to a given bound
-
User specified bounds
•
Number of nodes
•
Possible Values
-
Rationale : Find all error detectable with in bound
Tools Should avoid some equivalent inputs
Outline
Korat
oExamples
oWhat it does
oDemo
oHow it works
oResults
ASTGen
Conclusion
Example : Directed Acyclic Graph
User Provides Input representation (Java)
Class DAG {
List<DAGNode> nodes;
int size;
Static class DAGNode {
DAGNode[] children;
}
}
Desired Properties of Objects of these classes
-No Directed cycle among the nodes
-Not a multi-graph (all outgoing edges different)
Properties as Imperative Predicates
(desired structures)
•
•
Method that Identifies desired Structures
Takes an Input that can be desired or not (ex. Graph is a
DAG or not)
- Returns Boolean Indicating desirability
•
Advantages
- Familiar Language
- Existing development tools
- Predicates can be already present in the code
Example Finitization

specifies number of objects for each class



1 object for BST: { B0 }
3 objects for Node: { N0, N1, N2 }
specifies set of values for each field




sets consist of objects and literals
for root, left, right: { null, N0, N1, N2 }
for value: { 1, 2, 3 }
for size: { 3 }
Korat
Bonded-Exhaustive generation from imperative
predicates (Desired Structures)
Inputs: predicate and finitization.
Output: All Structures where predicate returns
true.
Korat Searches input space to find appropriate
structures
Korat
Implemented in Java
•Works on java predicates
Command line tool main arguments
• --Class main class for which to generate structures
•--Predicate : Method with test properties
•--Finitization : Method for finitization
•--args : bounds for finitization
Actions for generated structures
-Visualizing Structures
-Storing Structures in a file
-Running the code under test for each structure
Korat
java -cp korat.jar korat.Korat --visualize --class
korat.examples.binarytree.BinaryTree --args 3,3,3(runs
binary tree example)
java -cp korat.jar korat.Korat --visualize --class
korat.examples.searchtree.SearchTree --args
3,3,3,0,2(runs binary search tree example)
Running Example
import java.util.*;
class BinaryTree {
private Node root; // root node
private int size; // number of nodes in the tree
static class Node {
private Node left; // left child
private Node right; // right child
}
}
Running Example
public static Finitization finBinaryTree(int
NUM_Node) {
Finitization f = new Finitization(BinaryTree.class);
ObjSet nodes = f.createObjects("Node", NUM_Node);
// #Node = NUM_Node
nodes.add(null);
f.set("root", nodes);
// root in null + Node
f.set("size", NUM_Node);
// size = NUM_Node
f.set("Node.left", nodes); // Node.left in null + Node
f.set("Node.right", nodes); // Node.right in null+ Node
return f;
}
}
Running Example
public boolean repOk() {
// checks that empty tree has size zero
if (root == null) return size == 0;
Set visited = new HashSet();
visited.add(root);
LinkedList workList = new LinkedList();
workList.add(root);
while (!workList.isEmpty()) {
Node current = (Node)workList.removeFirst();
if (current.left != null) {
// checks that tree has no cycle
if (!visited.add(current.left))
return false;
workList.add(current.left);
}
if (current.right != null) {
// checks that tree has no cycle
if (!visited.add(current.right))
return false;
workList.add(current.right);
}
}
// checks that size is consistent
if (visited.size() != size) return false;
return true;
}
Example Valid Inputs

trees with exactly 3 nodes
B0: 3
B0: 3
root
root
N 0: 2
left
N 1: 1
B0: 3
root
N 0: 1
right
N 2: 3
B0: 3
root
N 0: 1
right
N 1: 2
right
N 2: 3
right
N 1: 3
left
N 2: 2
B0: 3
root
N 0: 3
N 0: 3
left
N 1: 1
left
N 1: 2
right
N 2: 2
left
N 2: 1
Validity Properties for Example

underlying graph is a tree
(no sharing between
subtrees)
B0: 3
root
N0 : 2


correct number of nodes
reachable from root
node values ordered
for binary search
left
N 1: 1
right
N 2: 3
Example Testing Scenario
Program for XML Processing
•Create a model for test inputs (XML Syntax
tree)
•Write predicates for valid inputs
•Korat generates valid inputs
•Translate from model to actual inputs (prettyprint)
Challenge for Generation
How to efficiently desired test inputs?
-Naturally input spaces can be
enumerated (eg: all graphs of given size)
-Sparce : number of desired test inputs
much smaller than the total number of
inputs (eg: #DAGs << #Graphs)
-Brute-force search is inferable  must
reason about the behavior of the predicate
Korat efficient generates all (valid) structures
within given bounds
- Systematically searches the bounded input
spaces
- Avoids some equivalent inputs
- prunes the search based on data accessed
during predicate execution
- Monitors dynamically what predicates
accesses
Input Space

all possible object graphs with a BST root
(obeying type declarations)
B0: 2
B0: 3
root
root
N0: 2
N0: 2
left
N1: 1
B0: 3
right
right
left
N1: 1
N2: 3
B0: 3
N2: 3
root
B0: 1
N0: 3
N0: 1
N0: 2
root
right
left
root
N1: 1
left
N1: 1
left
N2: 2
N2: 3
right
B0: 1
B0: 1
B0: 0
N0: 1
root
N0: 1
root
left
right
B0: 3
B0: 3
B0: 1
N0: 3
root
N0: 1
root
N0: 1
root
right
N1: 2
N1: 2
left
right
B0: 3
N2: 3
B0: 3
N2: 1
right
N0: 1
root
N1: 3
N2: 2
N0: 3
root
right
left
N1: 1
N2: 2
left
right
left
Isomorphic Inputs


equivalent for all code and all properties
example for trees: permutation of nodes
B0: 3
B0: 3
root
root

N 0: 2
left
N 1: 1

right
N 2: 3
N 1: 2
left
N 2: 1
right
N 0: 3
removing isomorphic inputs from test suites


significantly reduces the number of tests
does not reduce quality
Nonisomorphic Generation

simple “solution”



generate all inputs
filter out isomorphic inputs
Korat does not require filtering



generate only one (candidate) input from each
isomorphism class
only the lexicographically smallest input
search increments some field values for >1
Correctness

Korat’s input generation

sound


complete


no invalid input
at least one valid input from each isomorphism class
optimal

at most one (valid) input from each isomorphism class
Korat Structure Generation
very large input spaces
benchmark
size input
space
BST
8
12
253
292
HeapArray
6
8
220
229
java.util.LinkedList
8
12
291
2150
java.util.TreeMap
7
9
292
2130
java.util.HashSet
7
11
2119
2215
Korat Structure Generation
pruning based on filed accesses very effective
benchmark
size input candidate
space inputs
BST
8
12
253
292
54418
12284830
HeapArray
6
8
220
229
64533
5231385
java.util.LinkedList
8
12
291
2150
5455
5034894
java.util.TreeMap
7
9
292
2130
256763
50209400
java.util.HashSet
7
11
2119
2215
193200
39075006
Korat Structure Generation
correct number of nonisomorphic structures (Sloane’s)
benchmark
size input candidate valid
space inputs
inputs
BST
8
12
253
292
54418
12284830
1430
208012
HeapArray
6
8
220
229
64533
13139
5231385 1005075
java.util.LinkedList
8
12
291
2150
5455
4140
5034894 4213597
java.util.TreeMap
7
9
292
2130
256763
50209400
35
122
java.util.HashSet
7
2119
193200
2386
Korat Structure Generation
800Mhz Pentium III Sun’s Java 2 SDK 1.3.1 JVM
benchmark
size input candidate valid time
space inputs
inputs [sec]
BST
8
12
253
292
HeapArray
6
8
java.util.LinkedList
54418
12284830
1430
208012
2
234
220
229
64533
13139
5231385 1005075
2
43
8
12
291
2150
5455
4140
5034894 4213597
2
690
java.util.TreeMap
7
9
292
2130
256763
50209400
35
122
9
2149
java.util.HashSet
7
2119
193200
2386
4
Korat at Microsoft Research
Korat implemented in the AsmLT test tool in foundations of
software engineering group
- Predicates in Abstract state machine language (AsmL),
not in java or C#
- GUI for setting finitization and manipulating test
- Korat can be used stand-alone or to generate input for
method sequences
- Extensions
- (Controlled) non-exhaustive generation
- Generation of complete tests from partial tests
- Library for faster generation of common datatypes
AsmLT/Korat at Microsoft
Used by testers in several product groups
Enabling finding numerous errors
XML Tools
Xpath Compiler (10 error codes, test –suite agumentation)
Serialization (3 Error codes, Changing spec)
Web-Service protocols
WS-Policy (13 code errors, 6 problems in informal spec)
WS-Routing (1 code error, 20 problems in informal spec)
Others
SSL Stream
MSN Authentication, …...
Errors Found in
-
Important real world applications
-
Code already tested using best testing practices
Korat at Google
Testing Web traversal code
Test Inputs based on DAGs(Strongly connected
components of websites with links)
Problem : Large number of inputs
Goal : Faster generation and execution of
structurally complex test inputs
Challenge : Korat search mostly sequentially
Solution : Parallelized Korat Search
- A Family of (Online) Algorithms for load
balancing
ASTGen: Imperative Generators
Korat is Inherently declarative
- User specifies what inputs to generate, not how
- Predicates are declarative specifications written
in imperative code (Java)
ASTGen is imperative
- User Specifies how to generate inputs
- Write code that directly generates test inputs
instead of writing code that checks properties
- Faster generation and more involved
ASTGen
Framework rather than a tool
- User needs to extend if for specific purpose
- Based on NLP description of Input
First extension for generating abstract syntax
trees(ASTs) of Java Programs
- Applied on testing parts of two Popular
IDEs(refactoring engines NetBeans and
Eclipse)
Results : 47 Bugs (20 Eclipse and 17 NetBeans)
Related Testing Approaches
Model Based Testing
-
Predicates as specs (UML)
Specification Based Testing
-
Predicates as Specs, Bounded-exhaustive generation
Constraint based generation
-
Tools typically handle only primitive types not structures
Random Generation
- No guarantees, hard to generate inputs for sparse spaces
Grammar based Generation
-
Hard to navigate inputs with complex properties
Combinatorial selection (Pair-wise generation)
- Easy to enumerate spaces, smart selection of inputs
Conclusions
Korat automates specification-based testing

uses method precondition to generate all
nonisomorphic test inputs


prunes search space using field accesses
invokes the method on each input and uses
method postcondition as a test oracle
ASTGen is an imperative generator for ASTs, found
bugs in IDEs
Citations : Darko Marinov – Korat – a tool for generating
Structurally Complex Test Inputs