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
Detection method for finite satisfiability problems.
Identification method for finite satisfiability problem causes.
Disjoint Propagation method.
Description: FiniteSatUSE 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)
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.