UML class diagrams are a popular notation for modeling structural features. As there is just so much you can represent with a graphical notation, you typically need to enrich UML diagrams with integrity constraints using the Object Constraint Language (OCL). OCL is a textual notation that enables the definition of class invariants and pre/postconditions for operations.

This formalization can be added gradually, but as UML/OCL models grow more complex, it may be necessary to check that there are no inconsistencies, e.g., constraints that become unsatisfiable due to the interactions with other constraints. Detecting such errors is a complex task. There are a lot of different approaches to check the quality of constraints, each one with a different set of trade-offs (we obviously root for bounded verification approaches like EMFtoCSP).

But, if it is already challenging to detect that there is something wrong with your constraints, it is even harder to understand the “why” the constraints are inconsistent. And if you don’t know why they are failing, trying to repair the model by rewriting the incorrect constraints in a proper way will be a loooong process.

To help with this, we present MVM (Model Validator Mixer), a modeling tool for domain engineers that helps them locate, understand and fix consistency problems in UML/OCL class diagrams. To this end, MVM computes and organizes information about groups of inconsistent constraints and sample instances that satisfy most (but not all) integrity constraints. MVM is implemented as a plug-in for the UML Specification Environment (USE), a modeling environment offering advanced features for the verification and validation of UML/OCL models.

Each consistency error may be caused by a single incorrect invariant or an unintended interaction between several invariants. To this end, we will provide the following information to the domain engineer:

  • Minimal unsatisfiable cores: Sets of OCL invariants that cannot be simultane-ously satisfied and that become satisfiable if any member of the set is removed. While each unsatisfiable core is potentially an independent error, several cores that share some constraints may indicate a problem in the constraints included in their intersection.
  • Max-satisfiable constraints and instances: Sets of OCL invariants that can be satisfied as a whole, together with sample instances satisfying only those max-satisfiable constraints. The goal is showing the domain engineer what such instances would look like, in order to help him have a better idea of how the current constraints should be modified.
  • “What-if ” scenarios:  Sample instances that would be legal if one constraint in the unsatisfiable core is dropped. Again, the rationale is helping the do-main engineer figure out whether such instances should be made valid by rewriting the corresponding constraint.

You can see an example of the tool interface in the featured image for this post. Note how you can see in the rightmost tab which combinations are satisfiable if you eliminate a selected invariant. Also, double-clicking on any of the proposed combinations creates an object diagram with a sample valid instance.

The central idea of MVN is presenting all this information in a cohesive and usable way that helps the user understand the consistency problems that need to be ad-dressed, their causes and candidate repairs.

MVM will be presented at EMMSAD’22 as part of the tool paper A Tool for Debugging Unsatisfiable Integrity Constraints in UML/OCL Class Diagrams”. Pre-print available here.

Our future work will aim to improve the strategies to optimize the calculation, by introducing different strategies for enumerating unsatisfiable cores and proposing heuristics tailored for OCL invariants.

 

 

Interested in modeling?

Interested in modeling?

Follow the latest news on software modeling and low-code development

You have Successfully Subscribed!

Pin It on Pinterest

Share This