Verificación Formal de Programas

Mere som dette

NORMA TECNICA COLOMBIANA 4114

af MICHELL CAMARGO

Actividad integradora 2. Implicaciones tecnocientíficas. El celular

af Karla Lopez

Nomina.

af María Camila Wilches Parra

garantias individuales

af kevin yañes

Verificación Formal de Programas

Análisis de flujo de datos

Análisis de flujo de información

Seguimiento de flujos de datos sensibles

Identificación de filtraciones de información

Análisis de propagación de información

Análisis de flujo de control

Optimización de la estructura de control

Identificación de cuellos de botella

Análisis de rutas críticas

Análisis de dependencias

Resolución de dependencias circulares

Detección de ciclos de datos

Análisis de dependencia de datos

Garantías de calidad en software

Mejora continua del software

Recopilación de comentarios

Encuestas de satisfacción

Retroalimentación del usuario

Análisis estático de código

Revisión de código

Análisis de calidad de código

Análisis de código fuente

Pruebas de software

Pruebas de aceptación del usuario

Pruebas de integración

Pruebas funcionales

Modelado de sistemas

Verificación de concurrencia

Gestión de exclusión mutua

Detección de condiciones de carrera

Control de concurrencia

Verificación de rendimiento

Evaluación tiempo de ejecución

Análisis de uso de memoria

Optimización de recursos

Verificación de propiedades de sistemas

Auditoría de acceso

Análisis de vulnerabilidades

Seguridad y privacidad

Análisis de Algoritmos

Notación Asintótica

Eficiencia de un algoritmo

Tasa de crecimiento

Notación O (n²) Notación Ω (n) Notación Θ (n log n)

Tasa de Crecimiento de T(n)

Funciones lineales Cuadráticas y Exponenciales

Función de Tiempo respecto a n

Complejidad Computacional de Algoritmos

Memoria Utilizada

Tiempo de Ejecución

Mejor Caso y Peor Caso

Escenarios óptimos y pesimistas

Ordenamiento de burbuja

Estimación de Tiempo de Ejecución

Operaciones básicas de un algoritmo

Algoritmo de ordenamiento

Lógica de Hoare

Triplas de Hoare

Formato: {P} S {Q}

{P}Precondición {S}Instrucción {Q}Postcondición

Verificación de Programas Iterativos

Cota de Ciclo

Asegura que el ciclo terminará

Invariante de Bucle

Condición que es verdadera antes y después de cada iteración del bucle

Verificación de la Corrección de Programas

Pruebas formales Pruebas de ejecución

Corrección Parcial Corrección Total

Tipos de Instrucciones y sus Verificaciones

Composición Secuencial

Precondición más débil (wp): wp(S1, wp(S2, R))

Ejecuta instrucciones una tras otra.

Instrucción Condicional

Precondición más débil (wp): (C ⇒ wp(A, R)) ∧ (¬C ⇒ wp(B, R))

Ejecuta diferentes caminos de código según una condición.

Asignación

Precondición más débil (wp): R(x:=E) donde x es la variable y E la expresión.

Cambia el valor de una variable.

Instrucción Vacía

Precondición más débil (wp): Es igual a la poscondición.

No modifica el estado del programa.