MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams

In the context of Model Driven Engineering (MDE), the structure of a system is typically described by using a UML class diagram annotated with a set of Object Constraint Language (OCL) constraints. These constraints specify rules that are not expressible by using structural features. These constraints can be conflicting, resulting in inconsistencies. When this happens, the existing tools terminate and provide no information about which constraints are achievable and which ones cause conflicts. In this paper, we present MaxUSE, a tool for finding achievable OCL constraints and conflicts for inconsistent UML class diagrams. MaxUSE integrates the USE modeling tool with a satisfiability modulo theories (SMT) solver. It finds a set of achievable constraints based on their rankings by casting to a weighted MaxSMT problem and at the same time locates constraint conflicts. We use an example to demonstrate MaxUSE’s usage scenarios and discuss its usefulness to the community