Registro:
| Documento: | Tesis de Grado |
| Título: | Mejorando la usabilidad de herramientas de verificación |
| Título alternativo: | Improving usability of verification tools |
| Autor: | Chicote, Marcos José |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Fecha de defensa: | 2012-05-10 |
| Fecha en portada: | Mayo 2012 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Galeotti, Juan Pablo |
| Director Asistente: | Garbervetsky, Diego David |
| Jurado: | Braberman, Víctor Adrián; Bonomo, Flavia |
| Idioma: | Español |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000518_Chicote |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000518_Chicote.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000518_Chicote |
| Ubicación: | Dep.COM 000518 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Chicote, Marcos José. (2012). Mejorando la usabilidad de herramientas de verificación. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000518_Chicote |
Resumen:
TACO es una herramienta de código abierto que permite el análisis de programas Java realizando una verificación estática del código fuente contra una especificación en JML (Java Modeling Language) o JFSL (Java Forge Specification Language). TACO utiliza la técnica de verificación acotada en la que todas las ejecuciones de un procedimiento son examinadas hasta un límite provisto por el usuario que acota el espacio de análisis. TACO traduce código Java a JDynAlloy (un lenguaje de representación intermedia) que luego es traducido a DynAlloy para su verificación. En el presente trabajo se presentan diversas mejoras de usabilidad sobre la herramienta TACO que permiten un mayor y mejor análisis del contra ejemplo detectado luego de una verificación. Asimismo se presenta el diseño y desarrollo de un plugin para Eclipse, llamado TacoPlug, que utiliza y expande TACO para proveer una mejor experiencia de usuario y una mayor posibilidad de debugging. Si TACO detecta una violación a la especificación, TacoPlug la presenta en términos de código fuente anotado y brinda al usuario la posibilidad de localizar la falla mediante diversas vistas similares a las de cualquier software de debugging. Finalmente, se demuestra la usabilidad de la herramienta por medio de un ejemplo motivacional tomado de una porción de software industrial.
Abstract:
TACO is an open source verification tool that statically checks the compliance of a Java program against a specification written in JML (Java Modeling Language) or JFSL (Java Forge Specification Language). TACO uses a bounded verification technique, in which all executions of a procedure are examined up to a user-provided bound that narrows the analysis world. TACO translates Java annotated code to JDynAlloy (an intermediate language representation) which is then translated to DynAlloy for verification. In this work different improvements over usability issues on TACO are presented that enable a bigger and better analysis of a counterexample found in a verification. Furthermore, this thesis presents the design and implementation of an Eclipse’s plugin, called TacoPlug, that uses and expands TACO to provide a more user friendly experience and a profunder debugging capability. If TACO finds a specification violation, TacoPlug presents it in terms of the annotated source code and enables the user the posibility of localizing the defect through different views resembling any software debugger. Finally, the tool’s usability is shown by means of a motivational example taken from an industrial portion of software.
Citación:
---------- APA ----------
Chicote, Marcos José. (2012). Mejorando la usabilidad de herramientas de verificación. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000518_Chicote
---------- CHICAGO ----------
Chicote, Marcos José. "Mejorando la usabilidad de herramientas de verificación". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2012.https://hdl.handle.net/20.500.12110/seminario_nCOM000518_Chicote
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000518_Chicote.pdf
Distrubución geográfica
