Verificación formal

La verificación formal, en ingeniería y en computación, 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 lenguaje lógico (como la lógica de primer orden), se puede encontrar una demostración o prueba de corrección de un programa, algoritmo, etc, aunque también se puede encontrar su refutación.^[1]​Es un método necesario para probar cualquier programa o teoría pero, aunque sea satisfactoria, no asegura que la solución sea del todo correcta.

Dentro de la computación, la verificación es usada para estudiar los distintos sistemas software (en código fuente), sistemas combinacionales, circuitos digitales, etc.

Uno de los precursores de la verificación fue Edsger Dijkstra que, mostrando mucho interés en ella durante los 70, publicó el libro "A Discipline of Programming", en el cual, presentó su método de desarrollo sistemático de programas junto con sus pruebas de corrección, todos ellos basados en la verificación formal.

Importancia en las matemáticas

Tradicionalmente, dentro de las matemáticas, la verificación únicamente se utilizaba para la demostración y convicción de enunciados matemáticos y como medio de obtención de evidencias para la eliminación de dudas. Pero en la realidad tiene un mayor número de funciones, aparte de la de convicción:

• En su uso típico de convicción, como se ha dicho anteriormente, se basa en la demostración de enunciados y de conjeturas desconocidas, verificación deductiva. En este estudio, los matemáticos, además de partir de las premisas, construyen contraejemplos mediante una serie de pruebas, llamadas pruebas cuasi-empíricas, las cuales, intentan descubrir contradicciones o errores ocultos.

Uno de los métodos de esta verificación, es la llamada demostración deductiva, en donde la conclusión proviene de las premisas. Un defecto de esta demostración, es que se da lugar unos desarrollos tan extensos y complicados que el riesgo de cometer errores aumenta.

• Como método de sistematización. Aquí, la verificación no comprueba si algunas afirmaciones son ciertas o no, sino que se encarga de organizar enunciados individuales no relacionados. De esta manera, ayuda a identificar inconsistencias, a simplificar las teorías matemáticas (integrando afirmaciones y teoremas), a economizar los resultados, a ayudar a las aplicaciones mediante el análisis de sus axiomas y definiciones, etc.

• Como método de explicación. Aunque es posible alcanzar la afirmación mediante la verificación deductiva, en la mayoría de los casos, esta no proporciona una explicación válida de por qué puede ser verdadero y únicamente confirma que es verdad. Así, en los casos en los que los resultados están defendidos por evidencias cuasi-empíricas concluyentes, la función de la verificación no es únicamente la de convencer, sino también la de explicar. Más aún, para los matemáticos es más primordial este aspecto aclaratorio, que el simple hecho de verificación.

• Como verificación de modelos. Este tipo de verificación, consiste en un reconocimiento del modelo matemático (aplicable tanto para modelos finitos, como para modelos infinitos, ya que estos últimos se pueden representar de manera finita mediante la abstracción).

En definitiva, consiste en estudiar todos los cambios y estados de los modelos matemáticos mediante técnicas inteligentes de abstracción, consiguiendo agrupar en una sola operación todo el conjunto de estados. Estas transiciones estudiadas, son descritas en diferentes lógicas, tales como, la lógica computacional, la lógica temporal ...^[2]​

Importancia en el Software

En el software, la verificación formal de programas, consiste en justificar que un programa cumpla una especificación formal de su comportamiento. Esta verificación formal incluye la verificación deductiva, la interpretación abstracta, la demostración automática de teoremas, etc. La característica principal es que la verificación se escribe de manera dependiente al tipo de programación, es decir, las propias funciones incluyen sus especificaciones y el mismo código establece la corrección frente a esas especificaciones. Incluso, el propio lenguaje admite la verificación deductiva.

Otro enfoque complementario es la llamada derivación del programa, en la que un código eficiente se deriva, gracias a una serie de pasos de corrección, a partir de especificaciones funcionales.

Algunas características de las técnicas usadas en la verificación de programas son:

Las mismas propiedades, se pueden deducir lógicamente de la semántica.

También es posible obtener un único resultado a partir de todo el espacio de posibilidades, por ejemplo, buscar la solución únicamente en los números enteros y hasta un cierto número.

Y por último, estas técnicas tienen la característica de ser tanto decidibles, es decir, sus algoritmos están implementados para poner fin a una respuesta, como indecidibles (que nunca podrán terminar).

Estado actual

En la actualidad, la complejidad de los diseños de los algoritmos matemáticos aumenta día a día, es por eso, por lo que también aumenta la importancia de la verificación formal de la industria del hardware, la cual, es usada por la mayoría de las empresas líderes de hardware, más que por las del software.^[3]​ Esto es debido a que dentro del hardware los errores tienen una mayor importancia económica y comercial.

En el software, se utiliza la reparación automatizada de programas, que consiste en la corrección de errores software sin ninguna intervención humana. Esta reparación, utiliza las técnicas de la verificación formal (búsqueda de puntos del programa que pueden contener fallos o que pueden ser objetivos de síntesis) y también la de la síntesis de programas (reducir el espacio de búsqueda).

En el hardware, la cantidad de posibles interacciones entre los componentes, hace cada vez más difícil realizar las distintas posibilidades de simulación, es por ello, que el diseño del hardware sea más susceptible a los métodos de prueba automatizados, lo que hace más fácil la verificación formal. Morales, David (jul-sep 2003). «La investigación en verificación formal: un estado del arte». 

Véase también

• Lógica de Hoare, un sistema formal que permite la verificación de programas imperativos.
• Lenguajes formales.
• Método formal.
• Verificación de modelos.

Referencias

1. Nuevo Plan de Estudios Consultor Universal del Estudiante. Tomo de Matemáticas: Cultural, S. A. 2003. 
2. Davis, Philip J. (1983). The Mathematical Experience (en inglés). Great Britain:Pelican Books. 
3. Harrison, J: (2003). La verificación formal en Intel. 

Bibliografía

• Edsger Dijkstra, Wim H. J. Feijen, A Method of Programming, Addison-Wesley, 1988, 188 pages
• Gila Hanna, Más que demostración formal, 1989

Enlaces externos

• Verificación formal de algoritmos.
• Introducción a la verificación formal.
• Verificación formal de hardware.

•   Datos: Q173326