QMaxUSE: A new tool for verifying UML class diagrams and OCL invariants
Hao Wu
Abstract
Formal verification of a UML class diagram annotated with OCL constraints has been a long-standing challenge in Model-driven Engineering. In the past decades, many tools and techniques have been proposed to tackle this challenge. However, they do not scale well and are often unable to locate the conflicts when then number of OCL constraints significantly increases. In this paper, we present a new tool called QMaxUSE. This tool is designed for verifying UML class diagrams annotated with large number of OCL invariants. QMaxUSE is easy to install and deploy. It offers two distinct features. (1) A simple query language that allows users to choose parts of a UML class diagram to be verified. (2) A new procedure that is capable of performing concurrent verification.