28th IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems(FORTE 2008)
Tutorials
Tutorial I (10:00-13:00, June 10)
Wolfram Schulte (Microsoft Research),
Automating Software Testing Using Program Analysis
During the last ten years, code inspection for standard programming errors has largely been automated with static code analysis. During the next ten years, we believe we will see similar progress in automating testing, and specifically test generation, thanks to advances in program analysis, efficient constraint solvers and powerful computers. We present an overview of several related projects currently under way at Microsoft, and we will present one of them, namely PEX (see http://research.microsoft.com/pex/) in greater detail.
Note: Tutorial participants are recommended to install PEX in their laptop PCs before the tutorial starts. You can download PEX at http://research.microsoft.com/pex/
BIOGRAPHY
Wolfram Schulte is a principal researcher and currently leading the
software engineering efforts at Microsoft Research, Redmond, USA. His
group works in areas as diverse as experimental software engineering,
human interactions in programming, software reliability, programming
language design and implementation, as well as theorem
proving. Wolfram's main interest concerns the practical application of
formal techniques. He has published a variety of papers in the areas
of language design, verification, testing, program derivation and
compilation. Before joining Microsoft Research in 1999, Wolfram worked
at the University of Ulm (1993-1999), at sd&m, a German software
company (1992-1993), and at the Technical University Berlin
(1987-1992).
Tutorial II (14:30-17:30, June 10)
Antti Huima (Conformiq Software),
Automated Test Design with Conformiq Qtronic
This tutorial focuses on automated test design and model-based testing (MBT). We start with a short overview and a look on the general trends in MBT. There are various different ways to use models for testing and we survey the prominent ones, focusing on the following key issues:
- modeling test logic versus modeling desired system functionality
- infinite-state models versus abstraction and slicing
- level of test design automation reached
In addition, we have a look on the key research topics in automated test design, including:
- timed systems
- concurrency
- infinite-state systems
- scalability of test generation algorithms
In the second part of the tutorial we look at Conformiq Qtronic, a commercial software tool for automated test design that is driven by system models describing the functional requirements of systems under test. We mention shortly the main theoretical developments behind Qtronic, but focus in this tutorial on the practical aspects of using the tool and on our experiences from the industrial deployments, including:
- basic workflow for using the tool
- optimizing models for faster test generation and better coverage
- process improvement targets
Finally, we conclude the tutorial by looking at the process-level challenges and benefits of MBT, starting from our first-hand industrial experience but expanding then into a more general view. In this section we discuss e.g.:
- skill set evolution
- keeping testing independent
- common misconceptions about model-based testing and automatic test design
BIOGRAPHY
Mr. Antti Huima is the managing director and CTO for Conformiq
Software, one of the leading companies providing tools for automated
test design and model driven testing. He has ten years experience in the
IT industry and has lectured regularly on M.Sc. and postgraduate level -
for as long - on computer security and formal conformance testing; and
has served multiple program committees on the areas of formal methods
and testing. Many of the participants of this year's conference will
remember that Mr. Huima delivered last year's TESTCOM/FATES invited
plenary talk. Prior to starting with automated test design in 2001, Mr.
Huima worked in computer security as the research manager for SSH
Communications Security.

