28th IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems(FORTE 2008)


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/

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

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.