VERIFICACIÓN FORMAL DE PROGRAMAS

Plus de détails

Planeacion agregada

par Martín Gutiérrez Viana

EVOLUCION DEL TRABAJO

par Mayra Alejandra Rincon Perez

Producción material y simbólica en el Paleolítico

par irene zambrano

LA CREATIVIDAD Y EL ESPIRITU EMPRENDEDOR

par Dublas Muñoz

Se compone de

Herramientas de Verificación

Teorema de Invarianza

Regla 5: la cota del ciclo está acotada inferiormente.

Regla 4: la cota del ciclo disminuye con cada iteración.

Regla 3: la poscondición se cumple al finalizar la ejecución del ciclo.

Regla 2: el invariante se cumple justo después de cada iteración del ciclo.

Regla1: el invariante se cumple antes del inicio del ciclo.

Cota de Ciclo

Función entera t cuyo valor disminuye con cada iteración del ciclo y está acotada inferiormente

Medir el número de iteraciones restantes del ciclo

Invariante de Ciclo

Predicado P satisfecho justo antes y después de cada iteración del ciclo.

Proveer información relevante sobre el estado del programa

Coq Asistente de pruebas para el desarrollo de especificaciones formales y pruebas de corrección.

Frama-C Plataforma para análisis y verificación de código C.

SPARK Lenguaje y herramienta de verificación para sistemas críticos.

Limitaciones y Desafíos

Automatización: herramientas de verificación automática pueden ayudar pero no reemplazan el juicio humano.

Modelado Correcto: la especificación formal debe ser precisa y completa

Complejidad: el proceso puede ser complejo y tedioso para programas grandes.

Técnicas de Verificación

Inducción Matemática: para programas con estructuras repetitivas (ciclos).

Verificación Modular: descomponer el programa en módulos y verificar cada uno por separado.

Invariantes de Ciclo: propiedades que se mantienen verdaderas en cada iteración de un ciclo.

Proceso de Verificación

Paso 4: validar la tripla {Q}S{R} demostrando que Q ⇒ wp(S, R).

Paso 3: comprobar que la precondición inicial implica la precondición más débil derivada.

Paso 2: derivar la precondición más débil para cada instrucción del programa.

Paso 1: identificar la precondición y la poscondición.

Instrucciones Básicas

Composición Secuencia: ejecución de un conjunto de instrucciones en secuencia.

Instrucción Condicional: permite la ejecución de un conjunto de instrucciones basado en una condición.

Asignación: reemplaza el valor de una variable con el resultado de una expresión.

Instrucción Vacía: instrucción que no altera el estado del programa.

Determinar la condición inicial mínima necesaria para que el programa sea correcto respecto a su especificación

La precondición más débil es la condición más general que garantiza que la poscondición se cumple después de la ejecución del programa.

El formalismo para la especificación y verificación de programas.

{Precondición} Programa {Poscondición}

Que si la precondición es verdadera antes de la ejecución del programa, entonces la poscondición será verdadera después de la ejecución del programa.

Proceso de asegurar que un programa cumple con su especificación formal.

Garantizar la corrección del programa antes de su ejecución.

Del uso de técnicas matemáticas y lógicas.

Ejemplo

Precondición Más Débil (wp)

Tripla de Hoare

VERIFICACIÓN FORMAL DE PROGRAMAS