This part of the book is concerned with the theory of model-based testing where real systems are assumed to be modeled as labeled transition systems (and extensions thereof). Labeled transition systems were proposed by Keller [Kel76] and are widely used as underlying models for data-intensive systems (sequential and concurrent programs) as well as hardware circuits. The starting point of this form of model-based testing is a precise, unambiguous model description of the system under test. Based on this formal specification, test generation algorithms generate provably valid tests, i.e., tests that test what should be tested and no more than that. These algorithms provide automatic, faster and less error-prone test generation facilities. A sketch of the testing approach is given in Figure 9.