QMaxUSE: A query-based verification tool for verifying UML class diagrams with extreme size of OCL invariants.

Project maintained by classicwuhao Hosted on GitHub Pages — Theme by mattgraham


0. Latest Release

check out here for the latest changes and features of QMaxUSE.

1. Overview

QMaxUSE is an automated verification tool that is able to verify consistencies of a UML class diagram annotated with OCL invariants. QMaxUSE has two distinct features: (1) A query langauge that allows users to select parts of class diagram to be verified. (2) A powerful algorithm that is capable of performing concurrent verification on large number of complex OCL invariants. This is achieved by decomposing a large model into multiple queries.

2. Download and Run

Once you have JDK installed, you can just download QMaxUSE and run it without installing any additional libraries. QMaxUSE is a command-line based tool and currently supports Windows 10(x64), Ubuntu 20.04(x64) and macOS Big Sur(x64). If you would like to build your own version of QMaxUSE, please see here for details.

3. Running QMaxUSE on Windows 10 (x86/x64), Ubuntu 20.04(x64), macOS Big Sur (x64)

3.1 Solver Support

Currently, the latest version of QMaxUSE supports two solvers: z3 and cvc5 (for ubuntu and macOS). To switch between z3 and cvc5 for verification tasks, one can use the following command at QMaxUSE prompt:

	set-solver:<solver name>

Here, <solver name> can be either z3 or cvc5. If switch is successful, QMaxUSE will display a corresponding sovler’s version information.

3.2 Mode Switch

You can now specify two modes for verification. 1by1 mode allows QMaxUSE to verify one query at a time, other query verification will wait unitl the current thread finishes. async model allows QMaxUSE to use a pool of threads to verify multiple queries at a time, this yield much faster verification results. To switch between these two modes, you can use the following command at QMaxUSE prompt:


Here, <name> can be either 1by1 or async. By default, QMaxUSE uses 1by1 mode.

3.3 MaxUSE Support

QMaxUSE is fully compatible with MaxUSE. Everything is supported by MaxUSE is available in QMaxUSE including finding as many satisfiable features as possible and pinpointing all OCL conflicting constraints. However, you may need to setup Z3 for MaxUSE. See the instructions here. Technical details about how MaxUSE works are described here.


4.1 Issuing a query

Our query langauge allows users to issue a query to select parts of a class diagram to be verified. QMaxUSE accepts queries from command line. Here are some query examples:

4.2 Concurrent verification

QMaxUSE uses a specialised algorithm to decompose OCL invariants into multiple queries that can be verified concurrently. To use this feaure in QMaxUSE,


QMaxUSE’s verification procedures use Z3 SMT solver as its solving engine. To interact with Z3, it uses uran as its intermediate interfaces. Uran is responsible for generating well-formed SMT2 assertions and interpretation.

6. Benchmark

Overall, QMaxUSE improves up to 30x efficiency in verification. In particular, QMaxUSE performs very well on models with extreme size of OCL invariants. Try out some models from our benchmark.

7. Remarks

8. Papers:

Last updated: 31-May-2022