  The Unified Modeling Language (UML) is a widely used general purpose modeling
language. Together with the Object Constraint Language (OCL), formal models can
be described by defining the structure and behavior with UML and additional OCL
constraints. In the development process for formal models, it is important to
make sure that these models are (a) correct, i.e. consistent and complete, and
(b) testable in the sense that the developer is able to interactively check
model properties. The USE tool (UML-based Specification Environment) allows
both characteristics to be studied. We demonstrate how the tool supports
modelers to analyze, validate and verify UML and OCL models via the use of
several graphical means that assist the modeler in interpreting and visualizing
formal model descriptions. In particular, we discuss how the so-called USE
model validator plugin is integrated into the USE environment in order to allow
non domain experts to use it and construct object models that help to verify
properties like model consistency.
