User Assistance Characteristics of the USE Model Checking Tool
This work addresses the problem of making formal model checking more accessible and interactive for developers, particularly non-domain experts, in software engineering, though it appears incremental as it builds on existing USE tool features.
The paper tackles the challenge of ensuring correctness and testability in UML and OCL models by demonstrating how the USE tool, with its model validator plugin, assists modelers in analyzing, validating, and verifying these models through graphical means.
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.