En el contexto de los sistemas de hardware y software , la verificación formal es el acto de probar o refutar la corrección de los algoritmos previstos que subyacen a un sistema con respecto a una determinada especificación o propiedad formal, utilizando métodos matemáticos formales . [1]
La verificación formal puede ser útil para probar la corrección de sistemas tales como: protocolos criptográficos , circuitos combinacionales , circuitos digitales con memoria interna y software expresado como código fuente .
La verificación de estos sistemas se realiza proporcionando una prueba formal sobre un modelo matemático abstracto del sistema, siendo conocida por construcción la correspondencia entre el modelo matemático y la naturaleza del sistema. Ejemplos de objetos matemáticos que a menudo se usan para modelar sistemas son: máquinas de estado finito , sistemas de transición etiquetados , redes de Petri , sistemas de adición de vectores , autómatas cronometrados , autómatas híbridos , álgebra de procesos , semántica formal de lenguajes de programación como la semántica operativa , semántica denotacional ,semántica axiomática y lógica de Hoare . [2]
Un enfoque y formación es la verificación de modelos , que consiste en una exploración sistemáticamente exhaustiva del modelo matemático (esto es posible para modelos finitos , pero también para algunos modelos infinitos en los que conjuntos infinitos de estados pueden representarse efectivamente de forma finita mediante el uso de abstracción o aprovechando simetría). Por lo general, esto consiste en explorar todos los estados y transiciones en el modelo, mediante el uso de técnicas de abstracción inteligentes y específicas del dominio para considerar grupos completos de estados en una sola operación y reducir el tiempo de cálculo. Las técnicas de implementación incluyen enumeración de espacio de estado, enumeración de espacio de estado simbólico, interpretación abstracta , simulación simbólica , refinamiento de abstracción.[ cita requerida ] Las propiedades que deben verificarse a menudo se describen en lógicas temporales , como la lógica temporal lineal (LTL), el lenguaje de especificación de propiedades (PSL), las aserciones de SystemVerilog (SVA), [3] o la lógica de árbol computacional (CTL). La gran ventaja de la verificación de modelos es que a menudo es totalmente automática; su principal desventaja es que, en general, no escala a sistemas grandes; los modelos simbólicos normalmente se limitan a unos pocos cientos de bits de estado, mientras que la enumeración de estado explícita requiere que el espacio de estado que se explora sea relativamente pequeño.
Otro enfoque es la verificación deductiva. Consiste en generar a partir del sistema y sus especificaciones (y posiblemente otras anotaciones) una colección de obligaciones de prueba matemática , cuya verdad implica la conformidad del sistema con su especificación, y cumplir con estas obligaciones utilizando asistentes de prueba (probadores de teoremas interactivos) ( como HOL , ACL2 , Isabelle , Coq o PVS ) o probadores automáticos de teoremas , incluidas en particular las teorías del módulo de satisfacibilidad(SMT) solucionadores. Este enfoque tiene la desventaja de que puede requerir que el usuario comprenda en detalle por qué el sistema funciona correctamente y que transmita esta información al sistema de verificación, ya sea en forma de una secuencia de teoremas a probar o en forma de especificaciones ( invariantes, condiciones previas, condiciones posteriores) de los componentes del sistema (por ejemplo, funciones o procedimientos) y quizás subcomponentes (como bucles o estructuras de datos).
La verificación formal de los programas de software implica probar que un programa satisface una especificación formal de su comportamiento. Las subáreas de verificación formal incluyen verificación deductiva (ver arriba), interpretación abstracta , demostración automatizada de teoremas , sistemas de tipos y métodos formales ligeros . Un enfoque prometedor de verificación basada en tipos es la programación de tipos dependientes , en la que los tipos de funciones incluyen (al menos parte de) las especificaciones de esas funciones, y la verificación de tipos del código establece su corrección frente a esas especificaciones. Los lenguajes tipeados de forma dependiente con todas las funciones admiten la verificación deductiva como un caso especial.