Model-based testing for complex software systems is still an evolving field.
Typical modeling languages for test generation include UML, SysML, mainstream programming languages, finite machine notations, and mathematical formalisms such as Z, B (Event-B), Alloy or Coq.
The effectiveness of model-based testing is primarily due to the potential for automation it offers.
If a model is machine-readable and formal to the extent that it has a well-defined behavioral interpretation, test cases can in principle be derived mechanically.
Often the model is translated to or interpreted as a finite-state automaton or a state transition system.
To find test cases, the automaton is searched for executable paths.
Valuable off-nominal test cases may be obtained by leveraging unspecified transitions in these models.
This technique was first proposed by Offutt and Abdurazik in the paper that started model-based testing.
[3] Multiple techniques for test case generation have been developed and are surveyed by Rushby.
A solution found by solving the set of constraints formulas can serve as a test cases for the corresponding system.
Markov chains are an efficient way to handle Model-based Testing.
Usage models, so Markov chains, are mainly constructed of 2 artifacts : the finite-state machine (FSM) which represents all possible usage scenario of the tested system and the Operational Profiles (OP) which qualify the FSM to represent how the system is or will be used statistically.
Usage/Statistical Model Based Testing was recently extended to be applicable to embedded software systems.