Catálogo de publicaciones - tesis

Compartir en
redes sociales

Título de Acceso Abierto

Análisis de ejecuciones parciales de Software Model Checkers

Rodrigo Castaño Víctor A. Braberman

publishedVersion.

Resumen/Descripción – provisto por el repositorio digital
Las herramientas de análisis estático de código han mostrado un progreso significativo en la última década. Una de las formulaciones del problema a resolver es el de descubrir si una propiedad es satisfecha necesariamente por un determinado sistema bajo análisis o si, por el contrario, existen ejecuciones de dicho sistema que violan la propiedad deseada. Dicha enunciación del problema es conocida como Software Model Checking y el mismo es indecidible en el caso caso general. Habitualmente las herramientas de Software Model Checking buscan llegar a estar en condiciones de producir un resultado afirmativo, confirmando que la propiedad es satisfecha, o negativo, que habitualmente incluye un contraejemplo que viola la propiedad en cuestión. Sin embargo, en muchos casos, las herramientas se ven obligadas a producir un tercer resultado que indica que no se pudo demostrar la propiedad pero tampoco generar un contraejemplo. Además de los límites teóricos mencionados, en la práctica el problema resulta intratable para una gran cantidad de instancias de relevancia debido a que insume una elevada cantidad de recursos y de tiempo, incluso para casos en los que se alcanzaría finalmente una solución. En estos casos la gran mayoría de las herramientas indican al usuario únicamente que el intento de verificación no alcanzó un resultado concluyente, sin ninguna aclaración adicional. Este trabajo se centra en proveer al usuario información adicional en dichos intentos de verificación. Con ese objetivo en mente, proponemos distintas formas de presentar e interpretar la información que se puede extraer en esos casos, teniendo en cuenta distintos posibles grados de familiaridad con las técnicas de verificación subyacente por parte del usuario. En particular, nos centramos en una amplia familia de técnicas de verificación y presentamos varias vistas del progreso realizado por la herramienta previo a interrumpir el intento de verificación, acompañadas de su correspondiente caracterización formal. Adicionalmente, adaptamos la noción de cobertura, más frecuentemente utilizada en testing, a la familia de técnicas analizada. En ambos casos brindamos algoritmos que generan automáticamente tanto las vistas propuestas como sub-aproximaciones de la métrica de cobertura. Las técnicas propuestas son evaluadas sobre instancias de referencias ampliamente utilizadas tanto para determinar la practicalidad en cuanto al tiempo de ejecución requerido como para analizar la interpretabilidad de los resultados generados. La experimentación realizada confirma que es factible extraer información a partir de resultados inconcluyentes e interpretar dichos resultados revelando información no trivial.
Palabras clave – provistas por el repositorio digital

MODEL CHECKING; ANALISIS AUTOMATICO DE PROGRAMAS; COBERTURA; VERIFICACION FORMAL; PROGRAM ANALYSIS; COVERAGE; FORMAL VERIFICATION

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No requiere 2018 Biblioteca Digital (FCEN-UBA) (SNRD) acceso abierto

Información

Tipo de recurso:

tesis

Idiomas de la publicación

  • español castellano

País de edición

Argentina

Fecha de publicación

Información sobre licencias CC

https://creativecommons.org/licenses/by/2.5/ar/