Finite Satisfiability of UML Class Diagrams by Constraint Programming

Marco Cadoli, Diego Calvanese, Giuseppe De Giacomo, and Toni Mancini

In Proc. of the CP 2004 Workshop on CSP Techniques With Immediate Application. 2004.

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.


@inproceedings{CSPIA-2004,
   title = "Finite Satisfiability of UML Class Diagrams by Constraint
Programming",
   year = "2004",
   author = "Marco Cadoli and Diego Calvanese and De Giacomo, Giuseppe
and Toni Mancini",
   booktitle = "In Proc. of the CP 2004 Workshop on CSP Techniques With
Immediate Application",
}
pdf