Testmethode, bei der Testfälle automatisch aus einem formalen Modell des Systemverhaltens generiert werden.