Finite Satisfiability of UML class diagrams by Constraint Programming

Abstract

Finite model reasoning in UML class diagrams, e.g., checking whether a class is forced to have either zero or infinitely many objects, is of crucial importance for assessing quality of the analysis phase in software development. Despite the fact that finite model reasoning is often considered more important than unrestricted reasoning, no implementation of the former task has been attempted so far. The main result of this paper is that it is possible to use off-the-shelf tools for constraint modeling and programming for obtaining a finite model reasoner. In particular, exploiting appropriate reasoning techniques, we propose an encoding as a CSP of UML class diagram satisfiability. Moreover, we show also how CP can be used to actually return a finite model of a class diagram. A description of our system, which accepts as input class diagrams in the MOF syntax, and the results of the experimentation performed on the CIM knowledge base are given.