Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa

Abstract

Este documento aborda el problema de reducir la sobrecarga de supervisión del tiempo de ejecución para programas en los que se requiere una supervisión detallada de los eventos. Para ello complementamos modelar técnicas de verificación con métodos de razonamiento simbólico y mostrar que, bajo ciertas circunstancias, los fragmentos de código no afectan la validez de las propiedades subyacentes. Consideramos las propiedades de seguridad dadas como expresiones regulares sobre eventos generados por el programa. Además, mostramos cómo nuestro marco puede extenderse para considerar programas con ciclos. Probamos nuestra presentación con la ayuda del modelo Java PathFinder corrector [13].