QMaxUSE: A query-based verification tool for verifying UML class diagrams with extreme size of OCL invariants.
check out here for the latest changes and features of QMaxUSE.
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.
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.
java -jar qmaxuse.jar
to lanuch QMaxUSE.
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.
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:
set-mode:<name>
Here, <name> can be either 1by1 or async. By default, QMaxUSE uses 1by1 mode.
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.
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:
$select Person, Student.year, Student:study:Module.
Classes Person, Student and Module are selected. An attribute year (Student) is selected. An association study is selected. Note class Module is implicitly selected here because of study association.
$select Student.*, Student:*:Module
All attributes of Student class and any associations with association-ends Student and Module are selected.
$select Person, Student with Student::*
Classes Person, Student and all ocl invariants defined under Student class are selected. Further, all relevant clases, attributes and associations used in an ocl expression are also selected.
$select Student.* with Student::* but Student::inv4
All ocl invariants defined under Student class are selected except for inv4. Further, all relevant clases, attributes and associations used in an ocl expression are also selected.
$select Department, Asssignment, Student:finish:Assignment as query1
$select Student, Module with Student::* as query2
$query1 & query2
The first query has an alias query1. The second query has an alias query2. The last query is a joint query: query1 intersects query2. The intersection of two sets of feature are selected.
module QuerySet
select Person.*, Student.*, Module.*, Assignment:*:* with Student::*, Module::* but Person as class_query
end
The above query is saved in a query module called QuerySet. This query module is a part of (university) specification and it is automatically loaded when QMaxUSE reads this specification. A user can type
$QuerySet.class_query
to issue class_query. A query module can contain multiple aliased queries. Note that to reuse a query at a later stage, you must give a query an alias.
select Person.*, Student.* with Student::* inject {Student.allInstances()->forAll(s|s.modules->notEmpty())}
The above query is injected with an OCL invariant. The verification procedure will verify the query along with injected OCL. The verification will tell the consequences if the injected OCL invariant could break the consistencies or not. This is particularly useful for those who are not sure about adding an OCL invariant to a class whether will break the consistencies.
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.
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.
We woud like to thank our industrial partner LingCui Yu, HuangXin Xin and their teams from SYSUCC for helpful comments on this research.
Last updated: 31-May-2022
