Please use this identifier to cite or link to this item:
Title: Smart bound selection for the verification of UML/OCL class diagrams
Author: Clarisó Viladrosa, Robert  
González Pérez, Carlos Alberto
Cabot Sagrera, Jordi  
Others: University of Luxembourg
Universitat Oberta de Catalunya (UOC)
Universitat Oberta de Catalunya. Internet Interdisciplinary Institute (IN3)
Keywords: formal verification
class diagram
constraint propagation
Issue Date: 27-Nov-2017
Publisher: IEEE Transactions on Software Engineering
Citation: Clarisó, R., González, C.A. & Cabot, J. (2017). Smart Bound Selection for the Verification of UML/OCL Class Diagrams. IEEE Transactions on Software Engineering. doi: 10.1109/TSE.2017.2777830
Also see:
Abstract: 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.
Description: info:eu-repo/semantics/submittedVersion
Language: English
ISSN: 0098-5589MIAR
Appears in Collections:Articles

Files in This Item:
File Description SizeFormat 
Cabot_Smart_Bound.pdf876.17 kBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons