Smart bounded verification for UML / OCL models

Tweet about this on TwitterShare on FacebookBuffer this pageShare on RedditShare on LinkedInShare on Google+Email this to someone

Correctness of UML class diagrams annotated with OCL constraints can be checked using bounded veri cation, 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 veri cation 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-o ff between the veri fication time (faster for smaller domains) and the con fidence 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 veri cation 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 verifi cation tools and improve the efficiency of the veri fication process.

So basically we move from this verification process:

traditional bounded verification

to this one:

smart bounded verification

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

smartbounds

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:

Tweet about this on TwitterShare on FacebookBuffer this pageShare on RedditShare on LinkedInShare on Google+Email this to someone

Reply

Your email address will not be published. Required fields are marked *