Ground setting properties for an efficient translation of OCL in SMT-based model finding
Nils Przigoda, Robert Wille, Rolf Drechsler · 2016
Model Finding is an established method to increase the confidence in the correctness of a UML/OCL model, e. g., by automatically determining valid system states or counterexamples. In the recent past, numerous approaches have been proposed for this purpose. In order to cope with the underlying complexity, approaches based on satisfiability solvers have been found promising. They require a translation of all OCL constraints of the model for a corresponding solver.