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.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.
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 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).
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. 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».
Escribe un comentario o lo que quieras sobre Verificación formal (directo, no tienes que registrarte)
Comentarios
(de más nuevos a más antiguos)