In model-based testing, one of the biggest decisions taken
before modelling is the modelling language and the model analysis tool to
be used to model the system under investigation. UML, Alloy and Z are
examples of popular state-based modelling languages. In the literature,
there has been research about the similarities and the differences between
modelling languages. However, we believe that, in addition to recognising
the expressive power of modelling languages, it is crucial to detect the
capabilities and the weaknesses of analysis tools that parse and analyse
models written in these languages. In order to explore this area, we have
chosen four model analysis tools: USE, Alloy Analyzer, ZLive and ProZ
and observed how modelling and validation stages of MBT are handled
by these tools for the same system. Through this experiment, we not
only concretise the tasks that form the modelling and validation stages
of MBT process, but also reveal how efficiently these tasks are carried
out in different tools.