# User Assistance Characteristics of the USE Model Checking Tool

## TL;DR

The paper discusses how the USE tool supports modelers in analyzing, validating, and verifying UML and OCL models through graphical means and a plugin, enhancing usability for non-experts.

## Contribution

It introduces the USE model validator plugin and demonstrates its integration, improving accessibility and effectiveness in formal model checking.

## Key findings

- The USE tool facilitates interactive model analysis and validation.
- The plugin enables non-experts to verify model consistency.
- Graphical means aid in interpreting formal model descriptions.

## Abstract

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.