In [16, Section 16.6] some properties of a Mobile Maude application are model checked. This example is interesting because two levels of reflection (see Chapter 11) are involved: the object level, at which Mobile Maude system code executes, and the metalevel, at which application code is executed.
The model checker can also be executed in Full Maude. This is illustrated with an example in Section 15.7. This example, though quite simple, is interesting in several ways. The use of parameterization is exploited at both the system and the property level. At the system level, it allows a succinct specification of a parametric system. At the property level, it makes possible the specification of the relevant properties for each value of the parameter, also in a very succinct way. This is quite useful, because the property formulas vary as the parameter changes, and the parametric description encompasses an infinite number of instance formulas.