Smart bound selection for the verification of UML/OCL class diagrams

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.

La corrección de los diagramas de clase UML anotados con restricciones OCL puede verificarse usando técnicas de comprobación limitada, por ejemplo, resolución SAT o de programación con restricciones (CP). La comprobación limitada detecta los fallos de manera eficiente pero, por otro lado, la ausencia de fallos no garantiza un comportamiento correcto fuera del dominio delimitado. Por lo tanto, la elección de límites adecuados no es un proceso trivial, ya que hay una compensación entre el tiempo de verificación (más rápido para dominios más pequeños) y la seguridad en el resultado (mejor para dominios más grandes). Desafortunadamente, las herramientas de comprobación limitada proporcionan poco soporte en el proceso de selección vinculado. En este artículo, presentamos una técnica que puede usarse para (i) inferir automáticamente límites de verificación siempre que sea posible, (ii) ajustar un conjunto de límites propuestos por el usuario y (iii) guiar al usuario en el proceso de selección vinculado. Este enfoque puede aumentar la usabilidad de las herramientas de comprobación limitada UML/OCL y mejorar la eficiencia del proceso de verificación.

La correcció dels diagrames de classe UML anotats amb restriccions OCL es pot verificar usant tècniques de comprovació limitada, per exemple, resolució SAT o de programació amb restriccions (CP). La comprovació limitada detecta els errors de manera eficient però, d'altra banda, l'absència d'errades no garanteix un comportament correcte fora del domini delimitat. Per tant, l'elecció de límits adequats no és un procés trivial, ja que hi ha una compensació entre el temps de verificació (més ràpid per a dominis més petits) i la seguretat en el resultat (millor per a dominis més grans). Desafortunadament, les eines de comprovació limitada proporcionen poc suport en el procés de selecció vinculat. En aquest article, presentem una tècnica que pot usar-se per a (i) inferir automàticament límits de verificació sempre que sigui possible, (ii) ajustar un conjunt de límits proposats per l'usuari i (iii) guiar a l'usuari en el procés de selecció vinculat. Aquest enfocament pot augmentar la usabilitat de les eines de comprovació limitada UML/OCL i millorar l'eficiència del procés de verificació.