Please enable JavaScript.
Coggle requires JavaScript to display documents.
Verificación formal de programas, ¿QUE ES ?, Especificaciones Formales,…
Verificación formal de programas
Demuestrar que un programa informático cumple con sus especificaciones de manera matemática.
Esto implica usar técnicas y herramientas formales para analizar y asegurar que el programa funcionará correctamente bajo todos los posibles escenarios
Declaración formal de lo que el programa debe hacer.
Determinación de aspectos como la corrección funcional, seguridad y confiabilidad.
Representación abstracta del programa que permite verificar su comportamiento.
Modelos basados en lógica matemática (e.g., lógica de primer orden).
Modelos que pueden ser ejecutados en sistemas automáticos de verificación.
Métodos de Verificación Formal
Técnica que verifica todas las posibles ejecuciones de un programa a través de exploración exhaustiva.
Técnica que analiza el código sin ejecutarlo, detectando posibles errores o violaciones de especificaciones.
Método en el cual se demuestra matemáticamente la corrección de un programa.
Permite identificar errores antes de la fase de ejecución.
Se utiliza especialmente en sistemas donde la seguridad y confiabilidad son fundamentales.
Minimiza el costo de mantenimiento y depuración de software.
¿QUE ES ?
Especificaciones Formales
Modelos Formales
TIPÓS
LOGICO
ATOMATIZADOS
CHECKING
ANALISIS ESTATICO
TEOREMAS
VENTAJAS