Introduction
Model-Based Testing (MBT) can be defined as a methodology that uses models of systems under test (SUT) in test authoring. Test authoring usually takes the form of automatic test generation from models but can also happen as a result of SUT model simulation, where a user defines the stimuli sent to the system.
The following picture describes one of the more common flavors of the Model-Based Testing.

The process is specification-based. A user creates a model of the system under test using some formal modeling language supported by the tool based on the specification. This model is used to generate test cases automatically. The quality and size of the generated test suite depends on the directives provided by the user (e.g. coverage criteria or model exploration depth). Each test case contains both the stimuli to be sent to the system under test and the prediction of the outcome of applying those stimuli. The test execution prediction is based on the logic described by the model. The test cases may need to be translated to the executable scripts that are used by the test execution engine of choice. In case test execution results do not match the predicted one - there is a bug that needs to be fixed.
There are many various flavors of MBT. Some approaches do not generate a test suite in advance but create the next step of the test based on the execution result of the previous step. Other approaches do not predict the outcome of test cases which simplifies the modeling task significantly.
