Reasoning on UML Class Diagrams

Technical Report, Dipartimento di Informatica e Sistemistica, Università di Roma "La Sapienza". Technical Report 11-2003 2003.

UML is the de-facto standard formalism for software design and analysis. To support the design of large-scale industrial applications, sophisticated CASE tools are available on the market, that provide a user-friendly environment for editing, storing, and accessing multiple UML diagrams. It would be highly desirable to equip such CASE tools with automated reasoning capabilities in order to detect relevant formal properties of UML diagrams, such as inconsistencies or redundancies. With regard to this issue, we consider UML class diagrams, which are one of the most important components of UML, and we address the problem of reasoning on such diagrams. We resort to several results developed in the field of Description Logics (DLs), a family of logics that admit decidable reasoning procedures. Our first contribution is to show that reasoning on UML class diagrams is EXPTIME-hard, even under restrictive assumptions; we prove this result by showing a polynomial reduction from reasoning in DL. The second contribution consists in establishing EXPTIME-membership of reasoning on UML class diagrams, provided that the use of arbitrary OCL (first-order) constraints is disallowed. We get this result by using DLR ifd, a very expressive EXPTIME-decidable DL that is able to capture conceptual and object-oriented data models. The last contribution has a more practical flavor, and consists in a polynomial encoding of UML class diagrams in the DL ALCQI , which is the most expressive DL supported so far by DL-based reasoning systems. Though less expressive than DLR ifd, the DL ALCQI preserves enough semantics to keep reasoning about UML class diagrams sound and complete. Exploiting such an encoding, one can use current standard DL-based reasoning systems as core reasoning engines for equipping CASE tools with reasoning capabilities on UML class diagrams.

@techreport{TR-DIS-2003-11,
   title = "Reasoning on UML Class Diagrams",
   year = "2003",
   author = "Daniela Berardi and Andrea Calì and Diego Calvanese
and De Giacomo, Giuseppe",
   institution = "Dipartimento di Informatica e Sistemistica, Università
di Roma "La Sapienza"",
   number = "11-2003",
}