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)