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

Abstract

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.