Model-Based Testing is an approach for testcase generation for black-box testing. Model-based mutation testing was pioneered by Lipton in 1971. Since there have been several approaches described in literature, using several modelling formalisms and several commercial tools are available as well. Many applications of the approach are in the safety critical systems domain, probably because there the additional effort of creating a sufficiently complete model for testing is easier to argue.
The model-based mutation testing technique uses the input model to create a number of mutants, which differ from the original model in tiny details. The goal is then to find tests that differentiate the mutant from the original. These tests can then be used to test the implementation of the model.
An example would be a UML state machine that represents the behaviour of a car alarm system. The model would arm the alarm when the doors are lockend and raise an alarm when a door is open before the car is unlocked. This model could be used to derive tests over the input/output behaviour of the alarm system. These tests can be used to test a real-world implementation of the alarm system.