Testing and Model Generation

Motivation

Model-based approaches to development, verification (e.g., model checking and model based testing) and validation are becoming increasingly important in the software and hardware industry, since they appear to be one of the few ways in which the complexity of development and integration can be controlled. Models, however, are not always available. In particular, for legacy, third-party, or off-the-shelf components often no models are available, and if, in addition, the documentation is poor then it may be difficult or impossible to construct a valid model. Even for newly developed components, the construction of models typically requires specialized expertise and involves significant manual effort, implying that in practice often models are not available, or are not maintained and become outdated as the system evolves.

Model Generation

The goal of the project is to develop automated techniques to generate models of software components by observations of their behavior. The overall goal is that such techniques should be readily applicable to components of communication protocols, services, embedded, controllers, and other reactive systems that continuously interact with their environment. The resulting models will have the form of automata, often extended with facilities to model data manipulation and/or nonfunctional properties.
Our starting point is existing techniques for automata learning (aka. regular inference, e.g., as exemplified by the L* algorithm), which allow to construct finite-state automata models from observations of component behavior. A major challenge is to augment these techniques so that they become applicable to realistic systems. In particular, we focus on extending techniques for finite-state models to include data manipulation and/or nonfunctional properties.

Model Based Test Generation

We develop techniques and tools for generating test suites for communication protocols from models in the form of state machines.

Some Achievements

  • A general technique to specify coverage criteria in model-based test generation (FATES04)
  • First extensions of automata learning techniques to timed automata (see papers in FORMATS04, INFINITY04, CONCUR06, TCS11, and in Olga Grinchtein's Ph.D. thesis)
  • A novel approach to combine abstraction with automata learning in order to learn models of infinite-state components, which includes manipulation of data (ICTSS10)
  • A novel canonical automaton model which extends finite automata to include simple manipulations of and tests on data (ATVA11). The automaton model is based on a Nerode congruence, which means that learning algorithms for finite automata (i.e., regular languages) can be reused (almost) out-of-the-box for this richer class of models (VMCAI12)

Publications

(this list will be improved later)

Openings

We are looking for students to do M.Sc. projects:

Members

Current funding