Smart Bound Selection for the Verification of UML/OCL Class Diagrams





Publicado en

Actas de las XXIII Jornadas de Ingeniería del Software y Bases de Datos (JISBD 2018)


CC BY 4.0


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. This paper has been published in IEEE Transactions on Software Engineering []


Acerca de Clarisó, Robert

Palabras clave

Class Diagram, Constraint Propagation, Formal Verification, OCL, SAT, UML
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX