Correctness of UML class diagrams annotated with OCL constraints can be checked using bounded verication, e.g. SAT solvers (see an state of the art on static model verification tools for an overview on this topic and EMFtoCSP for details on our specific bounded verification approach).
Bounded verication detects faults efficiently but, on the other hand, the absence of faults does not guarantee a correct behavior outside the bounded domain. Hence, choosing suitable bounds is a non-trivial process as there is a trade-off between the verification time (faster for smaller domains) and the confidence in the result (better for larger domains).
Unfortunately, existing tools provide little support in this choice. Our approach consists in a technique that can be used to (i) automatically infer verication bounds whenever possible, (ii) tighten a set of bounds proposed by the user and (iii) guide the user in the bound selection process. This approach may increase the usability of UML/OCL bounded verification tools and improve the efficiency of the verification process.
So basically we move from this verification process:
to this one:
where our technique suggests potentially good bounds on behalf of the user by means of a series of size abstractions and bound propagations developed for OCL. These bounds can then be passed on the solver for a more efficient process
We have presented these ideas at SEFM’15 (13th International Conference on Software Engineering and Formal Methods). You can read the full paper here (free personal version).
See also the presentation below: