Tutorial at TAP 2008

Integrating Verification and Testing of
Object-Oriented Software

Prato, Italy, April 9th, 2008

Christian Engel, Christoph Gladisch, Vladimir Klebanov, Philipp Rümmer

Materials NEW

The slides of the tutorial are available as a printable PDF. The examples used in the tutorial are available below. Further materials, such as the KeY system itself, publications and details of the KeY book are available from the resp. sections of this website.

The examples used for the tutorial are available in this example archive. For running the examples from the general KeY introduction and the part "Test-Case Generation by Bounded Symbolic Execution" the standard KeY version 1.2 has been used. For the examples from "White-box testing by Combining Specification Extraction and Black-box Testing" and "Verification-based Test Case Generation with Loop Invariants and Method Specifications" the special KeY version KeY-1.1.175_SpecExtr.tgz is required.

Outline

Formal methods can only gain widespread use in industrial software development if they are integrated:

into software development techniques, tools, and languages used in practice
with each other.

A symbiosis of software testing and verification techniques is a highly desired goal, but at the current state of the art most available tools are dedicated to just one of the two tasks: verification or testing. We use the KeY system 1.2 (developed by the tutorial presenters) to demonstrate our approach in combining both.

KeY is an integrated deductive verification environment that allows full-functional verification of programs written in the industrial object-oriented language Java Card. At the core of the system is a novel interactive/automated theorem prover for the Dynamic Logic for Java. The prover has an easy-to-use graphical interface and seamlessly integrates automated and interactive proving. On the software development side, the system offers plug-ins for the industrial platforms Borland Together and Eclipse.

The KeY project is constantly working on techniques to increase the returns of verification in the industrial setting, including: proof reuse, symbolic debugging and verification-based testing.

The tutorial will cover the following topics:

How to design and formally specify object-oriented software (different fomalisms: UML/OCL, JML; tool support)
Deductive analysis of designs and specifications in the KeY prover
Deductive verification of non-trivial Java implementations with the KeY prover
Integration of verification and testing - why and how; generating JUnit tests from proofs

Schedule

This is a half-day tutorial. It is held on Wednesday morning, April 9th, 2008.