# A Formal Introduction to Model-Based Testing

Author: **Jan Peleska, Oliver Möller and Helge
Löding **

Abstract:

In this tutorial an introduction
to model-based testing is given. We start with a classical theorem by Chow who
showed that black-box tests can prove the equivalence of a system under test
(SUT) with its (finite, deterministic, untimed) automata specification, if an
upper bound of the number of internal SUT states is known. It is sketched how
this result could be generalised by Vaandrager et. al. to Timed
Automata. Since equivalence (i.e. bi-similarity) may be too restrictive as a
relation between specification and SUT, it is interesting to observe that a
similar approach is possible for process algebras such as CSP, CCS or Lotos
and the refinement relations defined for these algebraic models, as has first
been observed by Hennessy and de Nicola.
While these results provided very valuable insight into the theoretical
foundations of testing, equivalence testing requires to investigate so many
test cases that the practical applicability is very restricted (though
certainly not impossible, as an example from the field of "real-world" railway
control systems will show). As a consequence, it is interesting to investigate
the elaboration of test strategies which - though not capable of proving
equivalence between SUT and its specification - guarantee to come up with
"useful" test cases which can be automatically generated and executed within
acceptable time. We give an overview of the underlying heuristics of test
strategies that are relevant in the field of safety-critical embedded systems
testing. Moreover, the constraint solving problems associated with the test
case generation tasks are described, together with automated solver
techniques.

Tutorial, Part I (PDF file
(338KB)) and Tutorial, Part II (PDF file
(746KB) - with contributions by Oliver Möller and Helge Löding)