Hacia la construccion de drivers eficientes en bounded model checking mediante deteccion automatica de builders

Las técnicas que permiten mejorar la calidad del software producido son de vital importancia, sobre todo en sistemas críticos. Entre ellas, contamos con técnicas de verificación acotada de software, como el model checking de software, que permiten explorar exhaustivamente todas las ejecuciones posib...

Descripción completa

Detalles Bibliográficos
Autores principales: Politano, Mariano, Bengolea, Valeria S., Ponzio, Pablo Daniel, Aguirre, Nazareno Matías
Formato: Objeto de conferencia
Lenguaje:Español
Publicado: 2019
Materias:
Ciencias Informáticas
Drivers
Java PathFinder
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/91087
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-91087
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Español
topic Ciencias Informáticas
Drivers
Java PathFinder
spellingShingle Ciencias Informáticas
Drivers
Java PathFinder
Politano, Mariano
Bengolea, Valeria S.
Ponzio, Pablo Daniel
Aguirre, Nazareno Matías
Hacia la construccion de drivers eficientes en bounded model checking mediante deteccion automatica de builders
topic_facet Ciencias Informáticas
Drivers
Java PathFinder
description Las técnicas que permiten mejorar la calidad del software producido son de vital importancia, sobre todo en sistemas críticos. Entre ellas, contamos con técnicas de verificación acotada de software, como el model checking de software, que permiten explorar exhaustivamente todas las ejecuciones posibles del software con entradas de tamaño acotado, y reportar fallas encontradas durante el proceso. Para llevar a cabo la verificación acotada, los model checkers de software se basan en la definición de drivers: combinaciones de métodos que permiten construir las entradas con las que se ejecutará el programa. En este trabajo se observa que la selección de los métodos empleados en la definición del driver es de vital importancia para la verificación. Intuitivamente, es deseable seleccionar un conjunto de métodos tan pequeño como sea posible (para mayor eficiencia en el análisis), cuyas combinaciones permitan construir todas las estructuras acotadas para el módulo (para analizar el software con todas las entradas posibles). Esta selección de métodos, que usualmente se lleva a cabo de forma manual, no es una tarea fácil: requiere un análisis exhaustivo de las rutinas disponibles en el módulo y una comprensión profunda de la semántica de las mismas. En este trabajo se propone utilizar una herramienta automática para seleccionar un subconjunto de métodos relevantes de un módulo para la construcción de drivers eficientes para bounded model checking. Además, se evalúa el enfoque propuesto en el análisis de una propiedad particular del modulo Apache NodeCachingLinkedList, empleando el model checker Java PathFinder (JPF). Los resultados muestran que el enfoque de construcción de drivers presentado permite incrementar la eficiencia y la escalabilidad a estructuras de mayor tamaño en el análisis usando JPF.
format Objeto de conferencia
Objeto de conferencia
author Politano, Mariano
Bengolea, Valeria S.
Ponzio, Pablo Daniel
Aguirre, Nazareno Matías
author_facet Politano, Mariano
Bengolea, Valeria S.
Ponzio, Pablo Daniel
Aguirre, Nazareno Matías
author_sort Politano, Mariano
title Hacia la construccion de drivers eficientes en bounded model checking mediante deteccion automatica de builders
title_short Hacia la construccion de drivers eficientes en bounded model checking mediante deteccion automatica de builders
title_full Hacia la construccion de drivers eficientes en bounded model checking mediante deteccion automatica de builders
title_fullStr Hacia la construccion de drivers eficientes en bounded model checking mediante deteccion automatica de builders
title_full_unstemmed Hacia la construccion de drivers eficientes en bounded model checking mediante deteccion automatica de builders
title_sort hacia la construccion de drivers eficientes en bounded model checking mediante deteccion automatica de builders
publishDate 2019
url http://sedici.unlp.edu.ar/handle/10915/91087
work_keys_str_mv AT politanomariano hacialaconstrucciondedriverseficientesenboundedmodelcheckingmediantedeteccionautomaticadebuilders
AT bengoleavalerias hacialaconstrucciondedriverseficientesenboundedmodelcheckingmediantedeteccionautomaticadebuilders
AT ponziopablodaniel hacialaconstrucciondedriverseficientesenboundedmodelcheckingmediantedeteccionautomaticadebuilders
AT aguirrenazarenomatias hacialaconstrucciondedriverseficientesenboundedmodelcheckingmediantedeteccionautomaticadebuilders
bdutipo_str Repositorios
_version_ 1764820490681057283

Ejemplares similares