KeYTestGen2

PRE & y>x → {x:=y || y:=x}‹doA()› POST

Architectural overview

Java + JML

Test suite

Java + JML

Frontend

Java + JML

KeYTestGen Core

Backend

GUI

CLI

TestNG

XML

JUnit4

Capsule interface

Eclipse,

IntelliJ

Provides uniform API to backend implementations

Delegates and manages worker threads

Essential functionality is contained in autonomous subsystems of the core

Swing

POSIX compliant

Lightweight framework for delegating and monitoring worker threads.

Extends the Java executor model by providing wait-and-collect functionality, etc.

Abstract

test suite

Concrete

test suite

Bindings for custom implementations

1 ... Java classes

Coverage generator

Questions?

Set of symbolic execution nodes

Method worker

Class worker

Analyze symbolic execution tree, extract minimal set of nodes

satisfying given code coverage criteria

Get involved!

0 ... methods in class

Condition coverage

Decision coverage

Statement coverage

Branch coverage

Symbolic execution tree

Convert Java source file into

internal abstraction

Start and monitor method

workers

chrsva@chalmers.se

Generate test suite for

individual method

Start and monitor model generation, oracle generation and misc workers

Modified Condition / Decision Coverage

https://github.com/csvan/keytestgen

1... selected nodes

Model Generator

Model worker

Path condition

1

Generate concrete value bindings in order to satisfy path condition, and generate program heap abstraction

Generate a concrete

model for a single

execution path through

a single method.

KeY metadata

Java source

Java method

Model

Symbolic execution tree

Integers

Objects

Booleans

If inequalities are present in the code, enumeration is not possible, and integers will have to be dynamically generated

Object relations can be constructed through enumeration over the path condition itself

Like objects, boolean values are generated by enumeration

z

A : T

KeYStone

z == false & y == true

A != null & B == null & C == A

FALSE

Future work

Instance : T

Lightweight solver for real/integer constraints

B : T

Executes over 300x faster than previous SMT solution

Virtually no memory footprint (< 1MB/invocation)

y

TRUE

null

C : T

Two-phase simplex + integer relaxations

Can be extended to solve mixed-type problems (when KeY gains support for floats)

Natural state transitions

Synthesize "natural" construction of test

fixtures - get rid of all Java reflection.

Test mutations

KeY Interface

Oracle Generator

Postcondition

Oracle worker

Processes the postcondition of the method under test into an intermediary abstraction

Oracle

Generate an abstract

oracle for a single

method

KeY Core

Symbolic

Debugger

Current work

TestNG support

Front end

Features

Performance

Integration

Solve KeY bottleneck

Merge with symbolic debugger

KeYTestGen2

Same basic functionality but...

Timeline

faster

more configurable

support more target frameworks

separate from KeY codebase

Integrated with main KeY tool chain

KeYTestGen v.2

CHARTER project concludes. Development on KeYTestGen2 begins as complete re-implementation in order to address concerns over the previous version.

Beckert, Gladisch, Engel, Hähnle et al produce a series of papers on test case generation in KeY.

The Verification Based Test Generator (VBT) is created.

2012

2009

2006

The CHARTER project

VBT further developed and extended at Chalmers, with industrial use in mind. KeYTestGen v.1 created

Roadmap

KeYTestGen2

Background

Greyboxing in a KeY sort of way

Christopher Svanefalk

System overview

Towards automatic test case generation

Software Engineering using Formal Methods group,

Department of Computer Science and Engineering

Chalmers / University of Gothenburg

chrsva@chalmers.se

Generate symbolic execution tree

Current and future work

Extract subset of desired nodes from the tree

Generate test fixture satisfying the path

condition for each node

Encode everything as executable test suite

Symbolic execution gives us:

Complete mapping of execution paths

in the Java code

Information about program pre-state

constraints in order for a specific execution

path to be taken

How?

Why?

What?

KeYTestGen2 is an automatic, greybox (white + blackbox) test case generation system, engineered

to be useful in actual industrial contexts

KeY proof process yields extensive metadata about possible execution paths through Java programs

Use this data in order to generate test suites satisfying rigorous coverage criteria in a completely automatic fashion

The creation of robust test suites is usually

an error-prone, expensive element of

contemporary software engineering

Extend the flexibility of KeY by providing an alternative to strict formal verification:

automated test generation

Simple

Configurable

Extendable

Integrated with main KeY tool chain

PRE → ‹x=x+y; y=x-y; x=x-y; if(x>y) doA() else doB()› POST

Sequent

Symbolic execution

Oh yes!

KeY

KeY transforms Java + JML into sequents:

www.key-project.org

"Absolute" demonstration of correctness

φ → ‹π› ψ

Formal verification tool

PRE → {x:=y || y:=x}‹if(x>y) doA() else doB()› POST

φ → ‹π› ψ

Oh nopes!

/*@ public normal_behavior

@ requires PRE

@ ensures POST */

public void swapAndDo(int x, int y) {

x = x + y;

y = x - y;

x = x - y;

if (x > y) {

doA();

} else {

doB();

}

}

PRE & y<=x → {x:=y || y:=x}‹doB()› POST

KeY "executes" each statement in the Java code,

encoding its logical implications on the program state

Corresponds to program precondition

Transforms Java + JML contract into logical

proof obligation

Proof obligation closed using semi-automatic

theorem prover (based on a sequent calculus),

implying correctness of the code w.r.t. contract

Interactive: potentially requires (extensive)

training in logic and proof strategies

. . . . .

φ : antecedent (conjunction of formulae)

ψ : precedent (disjunction of formulae)

π : Java code

Corresponds to program postcondition

CLOSE

Limitations in KeY (no floats, no concurrency)

The proof may branch (on if-else statements for example), creating additional creating additional branches which must be closed to complete the proof

QED

Meeting half-way

Idea: use proof information generated by KeY in order to facilitate a less complete, but fully automatic verification technique: test case generation