Efficient reasoning about finite satisfiability of UML class diagrams with constrained generalization sets

UML class diagrams play a central role in the design and specification of software, databases and ontologies. The model driven architecture approach emphasizes the central role that models play, towards achieving reliable software. It is important that models are correct and that problems are detected as early as possible in the software design process. However, current case tools do not support reasoning tasks about class diagrams and enable the construction of erroneous models. There is an urgent need for methods for detecting analysis and design problems. In this paper, we present a linear programming based method for reasoning about finite satisfiability of UML class diagrams with constrained generalization sets. The method is simple and efficient and can be easily added to a case tool. It improves over existing methods that require exponential resources and extends them to new elements of class diagrams.