## 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