UMLtoCSP – Check the quality of your UML class diagrams with Constraint Programming

UMLtoCSP helps you to check that your UML class diagrams (extended with OCL constraints) satisfy a number of correctness properties, including weak and strong satisfiability (to make sure your model can be instantiated in a way that no constraints are violated) or absence of constraint redundancies among others. Unfortunately, these kind of mistakes are more common than you can imagine and even simple UML class diagrams with no OCL constraints may be wrong. For instance, can you guess why the following “trivial” model is plain wrong? (example taken from the book model-driven software engineering in practice)

UMLtoCSP works by translating the UML/OCL model into a Constraint Satisfaction Problem (CSP) that is evaluated using state-of-the-art constraint solvers to determine the correctness of the initial model. Choosing CSP as a target formalism for the verification has the key (for us) advantage that then the model verification process can be decidable, automatic and not limited to a certain subset of model constructs. But this does not come for free. As a trade-off, we must follow a a bounded verification approach which works by limiting the search space when verifying whether a given model satisfies a particular correctness property. You have all details in the paper but, in short, this means that results are only conclusive when a valid instance satisfying the correctness of the model is found. When it is not, we cannot be conclusive, either the valid instance is out of the search space considered or the model doesn’t verify that property.

Now (after too many years, I should say) we have published the full details of our approach in the paper “On the Verification of UML/OCL Class Diagrams using Constraint Programming” to appear in the Journal of Systems and Software (for those with no Elsevier access, you can download the unedited version of the paper here). We have developed also an open source tool implementing the ideas in the paper, called, obviously, the UMLtoCSP tool. The tool completely hides the verification process so a designer just needs to provide the input model and wait (sometimes a lot, but this is the topic of a future post) for the tool to give feedback. An evolution of this tool (integrated in the Eclipse IDE and adapted to deal with EMF models), called EMFtoCSP (you see, we are not very original naming tools 🙂 ) is also available.

UMLtoCSP has been developed together with Robert Clarisó and Daniel Riera as part of the GRES research group.