Reference : Smart Bound Selection for the Verification of UML/OCL Class Diagrams
Scientific journals : Article
Engineering, computing & technology : Computer science
Security, Reliability and Trust
Smart Bound Selection for the Verification of UML/OCL Class Diagrams
Clarisó, Robert mailto [Universitat Oberta de Catalunya > IT, Multimedia and Telecommunication Department]
Gonzalez Perez, Carlos Alberto mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Cabot, Jordi mailto [ICREA]
In press
IEEE Transactions on Software Engineering
Institute of Electrical and Electronics Engineers
Yes (verified by ORBilu)
New York
[en] Formal Verification ; Constraint Propagation ; Class Diagram
[en] Correctness of UML class diagrams annotated with OCL constraints can be checked using bounded verification techniques, e.g., SAT or constraint programming (CP) solvers. Bounded verification 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, bounded verification tools provide little support in the bound selection process. In this paper, we present a technique that can be used to (i) automatically infer verification 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.

File(s) associated to this reference

Fulltext file(s):

Limited access
TSE2777830.pdfAuthor preprint829.43 kBRequest a copy

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.