Verifying UML Models Annotated with OCL Strings

The Object Constraint Language (OCL) is a specification language that allows users to write precise constraints or rules over models that are built using the Unified Modeling Language (UML). Many OCL constraints used in real-world models specify a set of rules over string data types. This makes reasoning about UML models that are annotated with OCL string constraints very challenging. In this short paper, we demonstrate the feasibility of using Satisfiability Modulo Theories (SMT) solvers for verifying OCL string-type constraints. Specifically, we compare the string reasoning capabilities of three SMT solvers in terms of their usability, performance, and the diversity of instances generated. We believe that the Model-Driven Engineering (MDE) community can benefit from our preliminary results in identifying the strength and limitations of the state-of-the-art SMT solvers for OCL string verification.