Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10609/77126
Registro completo de metadatos
Campo DC Valor Lengua/Idioma
dc.contributor.authorClarisó, Robert-
dc.contributor.authorGonzález Pérez, Carlos Alberto-
dc.contributor.authorCabot, Jordi-
dc.contributor.otherUniversity of Luxembourg-
dc.contributor.otherUniversitat Oberta de Catalunya (UOC)-
dc.contributor.otherUniversitat Oberta de Catalunya. Internet Interdisciplinary Institute (IN3)-
dc.date.accessioned2018-05-02T09:37:22Z-
dc.date.available2018-05-02T09:37:22Z-
dc.date.issued2017-11-27-
dc.identifier.citationClarisó, 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-
dc.identifier.issn0098-5589MIAR
-
dc.identifier.urihttp://hdl.handle.net/10609/77126-
dc.description.abstractCorrectness 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.en
dc.description.abstractLa 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.es
dc.description.abstractLa 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ó.ca
dc.language.isoeng-
dc.publisherIEEE Transactions on Software Engineering-
dc.relation.urihttps://doi.org/10.1109/TSE.2017.2777830-
dc.rightsCC BY-NC-ND-
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/3.0/es/-
dc.subjectformal verificationen
dc.subjectUMLen
dc.subjectclass diagramen
dc.subjectOCLen
dc.subjectconstraint propagationen
dc.subjectSATen
dc.subjectverificación formales
dc.subjectverificació formalca
dc.subjectUMLca
dc.subjectUMLes
dc.subjectdiagrama de claseses
dc.subjectdiagrama de classesca
dc.subjectOCLca
dc.subjectOCLes
dc.subjectpropagación de restricciónes
dc.subjectpropagació de restriccióca
dc.subjectSATca
dc.subjectSATes
dc.subject.lcshSoftware engineeringen
dc.titleSmart bound selection for the verification of UML/OCL class diagrams-
dc.typeinfo:eu-repo/semantics/article-
dc.audience.mediatorTheme areas::Computer Science, Technology and Multimediaen
dc.subject.lemacEnginyeria de programarica
dc.subject.lcshesIngeniería de softwarees
dc.rights.accessRightsinfo:eu-repo/semantics/openAccess-
dc.identifier.doi10.1109/TSE.2017.2777830-
dc.gir.idAR/0000005936-
dc.type.versioninfo:eu-repo/semantics/submittedVersion-
Aparece en las colecciones: Articles cientÍfics
Articles

Ficheros en este ítem:
Fichero Descripción Tamaño Formato  
Cabot_Smart_Bound.pdf876,17 kBAdobe PDFVista previa
Visualizar/Abrir