Class diagram correctness Tools

FiniteSatUSE is a tool for reasoning about finite satisfiability problems in UML class diagrams. The tool provides verification methods for detection of finite satisfiability problems, identification of their causes and reasoning about disjoint and incomplete constraints.

Project name: FinteSatUSE

Project members: Victor Makarenkov, Rami Prilutsky, Vitaly Bichov, Michael Brichko Azzam Maraee.

Academic advisor: Prof. Mira Balaban

FiniteSatUSE Features

Detection method for finite satisfiability problems.

Identification method for finite satisfiability problem causes.

Identification method for problematic class hierarchy cycles.

Simplification Method

Disjoint Propagation method.


DescriptionFiniteSatUSE extends the USE system. The USE grammar that defines class diagrams is extended to support GS constraints, and qualifier, subsetting, redefinition and XOR constraints.

Examples (Detection, Identification and Propagation)

Electronic interlocking system domain

Molecular biology domain

Academic domain

Download files:

Scope and limitations:


Detection: class diagram with binary associations, class hierarchies, qualifier constraints, generalization set constraints, subsetting constraints, redefinition constraints and XOR constraints.

Identification: class diagram with binary associations and class hierarchy constraints.

Disjoint Propagation: class diagram with generalization set constraints.

Class Hierarchy Cycles Warning Method: class diagram with generalization set constraints.

Acknowledgments: We would like to thank USE developers for making their tool available for free.