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 their causes and reasoning about disjoint and incomplete constraints.
- Provide verification methods about finite satisfiability problems: Detection method for finite satisfiability problems, identification method for dangerous class hierarchy cycles, disjoint propagation method and identification method for finite satisfiability problem causes.
- 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.
Usefsverif works perfectly.