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

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].

• Autores: Cataño, Néstor
• Tipo de recurso: Trabajo de grado de pregrado
• Fecha de publicación: 2005
• Institución: Universidad Autónoma de Bucaramanga - UNAB
• Repositorio: Repositorio UNAB
• Idioma: eng
• OAI Identifier: oai:repository.unab.edu.co:20.500.12749/9027
• Acceso en línea: http://hdl.handle.net/20.500.12749/9027
• Palabra clave: Innovaciones tecnológicas; Ciencia de los computadores; Desarrollo de tecnología; Ingeniería de sistemas; Investigaciones; Tecnologías de la información y las comunicaciones; TIC´s; Technological innovations; Computer science; Technology development; Systems engineering; Investigations; Information and communication technologies; ICT's; Model checking; Java pathfinder; Symbolic reasoning; Instrumentation; Monitoring; Invariant strengthening; Innovaciones tecnológicas; Ciencias de la computación; Desarrollo tecnológico; Ingeniería de sistemas; Investigaciones; Tecnologías de la información y la comunicación; Comprobación de modelo; Buscador de rutas de Java; Razonamiento simbólico; Instrumentación; Supervisión; Fortalecimiento invariante
• License: Derechos de autor 2005 Revista Colombiana de Computación