Análisis de ejecuciones parciales de Software Model Checkers

Mostrar todas las versiones(3)

Las herramientas de análisis estático de código han mostrado un progresosignificativo en la última década. Una de las formulaciones del problema aresolver es el de descubrir si una propiedad es satisfecha necesariamente porun determinado sistema bajo análisis o si, por el contrario, existen ejecucio...

Descripción completa

Detalles Bibliográficos
Autor principal:	Castaño, Rodrigo
Otros Autores:	Braberman, Víctor A.
Formato:	Tesis doctoral publishedVersion
Lenguaje:	Inglés
Publicado:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2018
Materias:	MODEL CHECKING ANALISIS AUTOMATICO DE PROGRAMAS COBERTURA VERIFICACION FORMAL PROGRAM ANALYSIS COVERAGE FORMAL VERIFICATION
Acceso en línea:	https://hdl.handle.net/20.500.12110/tesis_n6345_Castano https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6345_Castano_oai
Aporte de:	Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires

id	I28-R145-tesis_n6345_Castano_oai
record_format	dspace
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-145
collection	Repositorio Digital de la Universidad de Buenos Aires (UBA)
language	Inglés
orig_language_str_mv	eng
topic	MODEL CHECKING ANALISIS AUTOMATICO DE PROGRAMAS COBERTURA VERIFICACION FORMAL MODEL CHECKING PROGRAM ANALYSIS COVERAGE FORMAL VERIFICATION
spellingShingle	MODEL CHECKING ANALISIS AUTOMATICO DE PROGRAMAS COBERTURA VERIFICACION FORMAL MODEL CHECKING PROGRAM ANALYSIS COVERAGE FORMAL VERIFICATION Castaño, Rodrigo Análisis de ejecuciones parciales de Software Model Checkers
topic_facet	MODEL CHECKING ANALISIS AUTOMATICO DE PROGRAMAS COBERTURA VERIFICACION FORMAL MODEL CHECKING PROGRAM ANALYSIS COVERAGE FORMAL VERIFICATION
description	Las herramientas de análisis estático de código han mostrado un progresosignificativo en la última década. Una de las formulaciones del problema aresolver es el de descubrir si una propiedad es satisfecha necesariamente porun 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 llegara estar en condiciones de producir un resultado afirmativo, confirmando quela 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áticamentetanto 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óna partir de resultados inconcluyentes e interpretar dichos resultados revelando información no trivial.
author2	Braberman, Víctor A.
author_facet	Braberman, Víctor A. Castaño, Rodrigo
format	Tesis doctoral Tesis doctoral publishedVersion
author	Castaño, Rodrigo
author_sort	Castaño, Rodrigo
title	Análisis de ejecuciones parciales de Software Model Checkers
title_short	Análisis de ejecuciones parciales de Software Model Checkers
title_full	Análisis de ejecuciones parciales de Software Model Checkers
title_fullStr	Análisis de ejecuciones parciales de Software Model Checkers
title_full_unstemmed	Análisis de ejecuciones parciales de Software Model Checkers
title_sort	análisis de ejecuciones parciales de software model checkers
publisher	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate	2018
url	https://hdl.handle.net/20.500.12110/tesis_n6345_Castano https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6345_Castano_oai
work_keys_str_mv	AT castanorodrigo analisisdeejecucionesparcialesdesoftwaremodelcheckers AT castanorodrigo analysisofpartialsoftwaremodelcheckingresults
_version_	1824355526535806976
spelling	I28-R145-tesis_n6345_Castano_oai2024-09-02 Braberman, Víctor A. Castaño, Rodrigo 2018-03-21 Las herramientas de análisis estático de código han mostrado un progresosignificativo en la última década. Una de las formulaciones del problema aresolver es el de descubrir si una propiedad es satisfecha necesariamente porun 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 llegara estar en condiciones de producir un resultado afirmativo, confirmando quela 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áticamentetanto 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óna partir de resultados inconcluyentes e interpretar dichos resultados revelando información no trivial. Static analysis tools have shown significant progress in the past decade. The problem these tools tackle can be formulated as deciding whether a property always holds for a specific system-under-verification or, on the contrary, certain execution in fact violates the desired safety property. Such problem definition is known as Software Model Checking and is, in the general case, undecidable. Software Model Checkers usually attempt to either prove the propertyholds or, when it does not, to produce a counterexample that constitutes aviolation. However, in many cases, tools produce neither and instead theyare forced to produce a third kind of result, indicating the attempt failedto produce a conclusive result, i.e. the property could not be proved but acounterexample was not found either. Taking the undecidability results aside,in practice the problem remains intractable for a large number of industrialinstances due to the immense resources required to solve them, even when aconclusive result would, at last, be produced. In all of these cases most tools would indicate, without any further clarifications, that the resource limits were reached and the result was inconclusive. This work aims to provide users with additional information in these cases. With that goal, we propose a number of approaches to presenting and interpreting the information that can be extracted from an inconclusive verification attempt. Moreover, we take into account the different possible degrees of expertise that a user could have with the underlying verification techniques and attempt to make our output understandable to all users. Concretely, we focus on a broad family of verification techniques andpresent a number of views of the progress achieved during verification. Weprovide, in each case, a formal characterization. Furthermore, we adapt thenotion of coverage, more commonly used in testing, to the family of verification techniques discussed. In both cases, we present algorithms to automatically compute both the views and the coverage metric proposed without requiring additional user input. The ideas proposed are evaluated on standard benchmark instances, bothto assess the practicality in terms of performance and also to determine theunderstandability of the results generated. Our experiments confirm that it is possible to extract information frominconclusive verification results and gather non-trivial insights from the results. Fil: Castaño, Rodrigo. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/tesis_n6345_Castano eng Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar MODEL CHECKING ANALISIS AUTOMATICO DE PROGRAMAS COBERTURA VERIFICACION FORMAL MODEL CHECKING PROGRAM ANALYSIS COVERAGE FORMAL VERIFICATION Análisis de ejecuciones parciales de Software Model Checkers Analysis of partial Software Model Checking results info:eu-repo/semantics/doctoralThesis info:ar-repo/semantics/tesis doctoral info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6345_Castano_oai

Análisis de ejecuciones parciales de Software Model Checkers

Ejemplares similares