Historia de Métodos formales

Un método formal es una técnica aplicada en el desarrollo de sistemas informáticos, con el fin de automatizar partes del proceso o dar prueba de la corrección del sistema.

Particularmente en sistemas criticas, errores en el software pueden tener efectos desastrosos: por ejemplo en el diseño de circuitos integrados y controladores de dispositivos o software integrado en vehiculos (militares). Hay una larga lista de errores en software con efectos dramaticos, algunos ejemplos notables son:

  • 1962: Un refuerzo salió de la pista durante el despegue, lo que resultó en la destrucción de la NASA Mariner 1. La causa era que un transcriptor faltó notar una barra encima de una letra en las especificaciones, resultando en la codificación de una fórmula incorrecta en su software de FORTRAN.
  • 1992: El primer F-22 Raptor se estrelló durante el aterrizaje en la Base Aérea Edwards, California. La causa del accidente resultó ser un error de software de control de vuelo.
  • 1996: La Agencia Espacial Europea 5 Vuelo 501 fue destruido 40 segundos después del despegue (4 de junio de 1996). El prototipo de cohete de 1 billón de dollares se autodestruyó debido a un error en el software de guiado de a bordo. [4]
  • 1999: NASA Mars Polar Lander fue destruida debido a que su programa tomó turbulencias atmosféricas como señal para haber aterrado, y apaguo los motores 40 metros encima de la superficie de Marte.

A partir de los sesentas, matematicos y informaticos se dedicaron a developear métodos matematicos para analizar y describir programes mientras declaraciones logicas. Algunos ejemplos son la analisis de programes mientras precondiciones y postcondiciones (Lógica de Hoare, 1969), o la Semántica de transformación de predicados introducido por Edsger Dijkstra en 1975.

Hay diferentes niveles de métodos formales:

Especificación formal

Una especificación formal es una descripcion de un sistema que utiliza totaciónes matemáticas para describir precisamente las propiedades que dicho sistema debe tener, sin preocuparse por la forma de obtener estas propiedades: “Describe lo que el sistema debe hacer sin decir cómo se va a hacer.”

Verificación formal

La verificación formal es un método de validación estática (se valida a través del propio código del programa, a partir de una abstracción o de una representación simbólica), en el que partiendo de un conjunto axiomático, reglas de inferencia y algún lenguage lógico (como la lógica de primer orden u otra de preferencia una lógica sólida y completa), se puede encontrar una demostración o prueba de corrección de un programa.

Demostración automática de teoremas

Demostración automática de teoremas se encarga de la demostración de teoremas matemáticos mediante programas de ordenador. Se utiliza principalmente en el diseño y la verificación de circuitos integrados, por la industria electrónica. Desde el bug FDIV del Pentium, la sofisticada y complicada unidad de punto flotante de los microprocesadores modernos se han diseñado utilizando pasos de escrutinio adicional. En los más modernos procesadores de AMD, Intel, y otros, se ha utilizado el demostrador automatizado de teoremas para verificar que las operaciones matemáticas de división y otras han sido diseñadas correctamente.

Publicado en Tecnologías Etiquetado con: