Introducción a la verificación formal

La prueba de software se conoce también como verificación y validación (V&V).

Es asegurar que el sistema de software cumpla las necesidades del usuario

 
Diferencias: 

• Verificación: 

Se conoce como un conjunto de actividades que aseguran que el software implementa correctamente una función especifica, esto nos lleva a cuestionar, ¿Estamos construyendo el producto correctamente?. El software debe estar conforme a las especificaciones.

• Validación:  

¿Se esta construyendo el producto adecuado?"El software debe hacer lo que el usuario requiere. 

Verificación estática y dinámica

•  Verificación dinámica: Se refiere al ejercicio y observación del comportamiento del producto (prueba). 
• Verificación estática: Se refiere al análisis de la representación estática del sistema para descubrir problemas. 

Los procesos de validación y verificación se inician con revisiones de requerimientos, luego se realizan revisiones del diseño e inspecciones de código hasta llegar a la prueba del producto.

El objetivo del proceso de V&V es garantizar la seguridad de que el sistema software esta “hecho para un propósito “, lo cual significa que el sistema debe ser suficientemente bueno para su uso establecido.

  

Pruebas de programas 

Las técnicas dinámicas también conocidas como testing(prueba) se basa en ejercitar una implementación. 

• Puede revelar la presencia de errores no su ausencia
• Una prueba exitosa consiste en descubrir uno o mas errores
• Solo se considera la técnica de validación para requerimientos no-funcionales
• De se usada en conjunto con la verificación estática 

•  Pruebas estadística: Pruebas diseñadas para reflejar la frecuencia de las entradas del usuario.Usadas para estimación de la confiabilidad. 

• Prueba de defectos: Pruebas diseñadas para descubrir defectos en el sistema. Una prueba de defectos exitosa es aquella que revela la presencia de defectos en el sistema.  

Depuración 

• La prueba de defectos y la depuración son distintos procesos
• La prueba de defectos se refiere a la confirmación de la presencia de errores
• La depuración se refiere a la localización y reparación de estos errores.
• La depuración involucra la formulación de una hipótesis acerca del comportamiento del programa y la prueba de la hipótesis para encontrar los errores en el sistema.  

Fases de pruebas

• Pruebas de unidades: prueba de componentes individuales. 
• Pruebas de módulos: prueba de conjuntos de componentes dependientes.
• Pruebas de sub-sistemas: prueba de colecciones de módulos integrados en sub-sistemas.
• Prueba del sistema: prueba del sistema completo ante de su entrega
• Prueba de aceptación: pruebas de los usuarios para verificar que el sistema cumple con los requerimientos. Llamado en ocasiones prueba alfa.  

Ejemplos de mala validación.

1. Marinero sin rumbo (1962)
 
Coste: 18,5 millones de dólares.

Desastre: El cohete Mariner 1, en una investigación espacial destinada a Venus, se desvió de su trayectoria de vuelo poco después de su lanzamiento. El control de la misión destruyó el cohete pasados 293 segundos desde el despegue.

Causa: Un programador codificó incorrectamente en el software una fórmula manuscrita, saltándose un simple guión sobre una expresión. Sin la función de suavizado indicada por este símbolo, el software interpretó como serias las variaciones normales de velocidad y causó correcciones erróneas en el rumbo que hicieron que el cohete saliera de su trayectoria.  El fallo del Pentium en las divisiones largas (1993)
 

Coste: 475 millones de dólares, credibilidad de Intel.

Desastre: el promocionadísimo chip de Intel, Pentium, producía errores al dividir números en coma flotante que se encontraban en un rango determinado. Por ejemplo, dividiendo 4195835,0/3145727,0 se obtenía 1,33374 en lugar de 1,33382, un error del 0,006%. Aunque el error afectaba a pocos usuarios, se convirtió en una pesadilla en cuanto a sus relaciones públicas; con unos 5 millones de chips en circulación, Intel ofreció reemplazar los Pentium sólo de aquellos clientes que demostraran que necesitaban alta precisión en sus cálculos. Finalmente, reemplazó los chips de todos los que lo solicitaron.

Causa: El divisor en la unidad de coma flotante contaba con una tabla de división incorrecta, donde faltaban cinco entradas sobre mil, y que provocaba estos errores en los redondeos. 
Referencias:  
Validación y Verificación  
Pruebas