Please enable JavaScript.
Coggle requires JavaScript to display documents.
Verificación Formal de Programas - Coggle Diagram
Verificación Formal de Programas
Programas (Conjunto de instrucciones)
Modelos (Abstracciones del sistema)
Sistemas embebidos (Software en dispositivos)
Sistemas computacionales (Software complejo)
Herramientas (Software de análisis)
Verificadores de modelos (Exploran estados posibles)
Demostradores de teoremas (Pruebas interactivas)
Análisis estático (Detecta errores sin ejecutar)
Métodos de Verificación (Estrategias de prueba)
Verificación deductiva (Deducción lógica)
Chequeo de modelos (Automático y exhaustivo)
Autómatas (Modelos secuenciales)
Invariante de ciclo (Se mantiene en bucle)
Cota de terminación (Valor decrece y finaliza)
Corrección parcial (Correcto si termina)
Corrección total (Además garantiza terminación)
Comparación con pruebas empíricas
Verificación formal (Prueba matemática sin ejecutar código)
Prueba empírica (Ejecución real con casos de prueba)
Especificaciones (Requisitos formales)
Propiedades (Funcionales y no funcionales)
Semántica formal
Lógicas de especificación (Formalizan requisitos)
Precondición (Condición inicial esperada)
Poscondición (Estado esperado tras ejecución)
Acercamientos (Métodos teóricos)
Teoría de tipos (Coherencia de datos)
Lógica de Hoare ({P} C {Q})
Aplicaciones (Usos en sistemas críticos)
Medicina (Dispositivos médicos)
Aeronáutica (Sistemas de vuelo)
Finanzas (Transacciones seguras)