Verificación de modelos

En informática , la verificación de modelos o verificación de propiedades es un método para comprobar si un modelo de estados finitos de un sistema cumple con una especificación dada (también conocida como corrección ). Esto se asocia típicamente con sistemas de hardware o software , donde la especificación contiene requisitos de vivacidad (como evitar el bloqueo mutuo ) así como requisitos de seguridad (como evitar estados que representen un fallo del sistema ).

Para resolver un problema de este tipo algorítmicamente , tanto el modelo del sistema como su especificación se formulan en un lenguaje matemático preciso. Con este fin, el problema se formula como una tarea lógica , es decir, comprobar si una estructura satisface una fórmula lógica dada. Este concepto general se aplica a muchos tipos de lógica y a muchos tipos de estructuras. Un problema sencillo de verificación de modelos consiste en comprobar si una fórmula en la lógica proposicional es satisfecha por una estructura dada.

La comprobación de propiedades se utiliza para verificar cuando dos descripciones no son equivalentes. Durante el refinamiento , la especificación se complementa con detalles innecesarios en la especificación de nivel superior. No es necesario verificar las propiedades recién introducidas con respecto a la especificación original, ya que esto no es posible. Por lo tanto, la estricta comprobación de equivalencia bidireccional se relaja a una comprobación de propiedades unidireccional. La implementación o el diseño se consideran un modelo del sistema, mientras que las especificaciones son propiedades que el modelo debe satisfacer. ^{[ 2 ]}

Se ha desarrollado una clase importante de métodos de verificación de modelos para comprobar modelos de diseños de hardware y software donde la especificación viene dada por una fórmula de lógica temporal . El trabajo pionero en la especificación de lógica temporal fue realizado por Amir Pnueli , quien recibió el premio Turing de 1996 por su "trabajo fundamental que introdujo la lógica temporal en la ciencia de la computación". ^{[ 3 ]} La verificación de modelos comenzó con el trabajo pionero de EM Clarke , EA Emerson , ^{[ 4 ] [ 5 ] [ 6 ]} por JP Queille y J. Sifakis . ^{[ 7 ]} Clarke, Emerson y Sifakis compartieron el premio Turing de 2007 por su trabajo fundamental que fundó y desarrolló el campo de la verificación de modelos. ^{[ 8 ] [ 9 ]}

La verificación de modelos se aplica con mayor frecuencia a diseños de hardware. En el caso del software, debido a la indecidibilidad (véase la teoría de la computabilidad ), el enfoque no puede ser completamente algorítmico, aplicarse a todos los sistemas ni proporcionar siempre una respuesta; en general, puede fallar al probar o refutar una propiedad dada. En el hardware de sistemas embebidos , es posible validar una especificación entregada, por ejemplo, mediante diagramas de actividad UML ^{[ 10 ]} o redes de Petri interpretadas por control ^{[ 11 ]} .

La estructura se suele proporcionar como una descripción de código fuente en un lenguaje de descripción de hardware industrial o un lenguaje de propósito específico. Dicho programa corresponde a una máquina de estados finitos (FSM), es decir, un grafo dirigido compuesto por nodos (o vértices ) y aristas . A cada nodo se le asocia un conjunto de proposiciones atómicas, que normalmente indican qué elementos de memoria son uno. Los nodos representan estados de un sistema, las aristas representan posibles transiciones que pueden alterar el estado, mientras que las proposiciones atómicas representan las propiedades básicas que se cumplen en un punto de ejecución. ^{[ 12 ]}

Formalmente, el problema se puede plantear de la siguiente manera: dada una propiedad deseada, expresada como una fórmula de lógica temporal${\displaystyle p}$y una estructura${\displaystyle M}$con estado inicial${\displaystyle s}$, decidir si${\displaystyle M,s\models p}$. Si${\displaystyle M}$es finito, como ocurre en el hardware, la verificación de modelos se reduce a una búsqueda en grafos .

En lugar de enumerar los estados alcanzables uno por uno, el espacio de estados a veces se puede recorrer de manera más eficiente considerando un gran número de estados en un solo paso. Cuando dicho recorrido del espacio de estados se basa en representaciones de un conjunto de estados y relaciones de transición como fórmulas lógicas, diagramas de decisión binarios (BDD) u otras estructuras de datos relacionadas, el método de verificación de modelos es simbólico .

Históricamente, los primeros métodos simbólicos utilizaron BDD . Tras el éxito de la satisfacibilidad proposicional en la resolución del problema de planificación en inteligencia artificial (véase satplan ) en 1996, el mismo enfoque se generalizó a la verificación de modelos para lógica temporal lineal (LTL): el problema de planificación corresponde a la verificación de modelos para propiedades de seguridad. Este método se conoce como verificación de modelos acotada. ^{[ 13 ]} El éxito de los solucionadores de satisfacibilidad booleana en la verificación de modelos acotada condujo al uso generalizado de solucionadores de satisfacibilidad en la verificación de modelos simbólica. ^{[ 14 ]}

Las herramientas de verificación de modelos se enfrentan a una explosión combinatoria del espacio de estados, comúnmente conocida como el problema de la explosión de estados , que debe abordarse para resolver la mayoría de los problemas del mundo real. Existen varios enfoques para combatir este problema.

1. Los algoritmos simbólicos evitan construir explícitamente el grafo para la máquina de estados finitos (FSM); en su lugar, lo representan implícitamente mediante una fórmula en lógica proposicional cuantificada. El uso de diagramas de decisión binarios (BDD) se popularizó gracias al trabajo de Ken McMillan, ^{[ 16 ]} así como de Olivier Coudert y Jean-Christophe Madre, ^{[ 17 ]} y el desarrollo de bibliotecas de manipulación de BDD de código abierto como CUDD ^{[ 18 ]} y BuDDy. ^{[ 19 ]}
2. Los algoritmos de verificación de modelos acotados despliegan la máquina de estados finitos durante un número fijo de pasos,${\displaystyle k}$y comprobar si puede producirse una infracción de propiedad en${\displaystyle k}$o menos pasos. Esto normalmente implica codificar el modelo restringido como una instancia de SAT . El proceso puede repetirse con valores cada vez mayores de${\displaystyle k}$hasta que se hayan descartado todas las posibles violaciones (cf. Búsqueda en profundidad iterativa ).
3. La abstracción intenta demostrar propiedades de un sistema simplificándolo primero. El sistema simplificado generalmente no satisface exactamente las mismas propiedades que el original, por lo que puede ser necesario un proceso de refinamiento. Por lo general, se requiere que la abstracción sea sólida (las propiedades demostradas en la abstracción son verdaderas para el sistema original); sin embargo, a veces la abstracción no es completa (no todas las propiedades verdaderas del sistema original son verdaderas para la abstracción). Un ejemplo de abstracción es ignorar los valores de las variables no booleanas y considerar solo las variables booleanas y el flujo de control del programa; dicha abstracción, aunque pueda parecer burda, puede, de hecho, ser suficiente para demostrar, por ejemplo, propiedades de exclusión mutua .
4. El refinamiento de abstracción guiado por contraejemplos (CEGAR) comienza la verificación con una abstracción gruesa (es decir, imprecisa) y la refina iterativamente. Cuando se encuentra una violación (es decir, un contraejemplo ), la herramienta analiza su viabilidad (es decir, ¿la violación es genuina o el resultado de una abstracción incompleta?). Si la violación es viable, se informa al usuario. Si no lo es, la prueba de inviabilidad se utiliza para refinar la abstracción y la verificación comienza de nuevo. ^{[ 20 ]}

Las herramientas de verificación de modelos se desarrollaron inicialmente para razonar sobre la corrección lógica de los sistemas de estados discretos , pero desde entonces se han ampliado para abordar sistemas híbridos de tiempo real y de formas limitadas .

La verificación de modelos también se estudia en el campo de la teoría de la complejidad computacional . Específicamente, se fija una fórmula lógica de primer orden sin variables libres y se considera el siguiente problema de decisión :

Dada una interpretación finita , por ejemplo, una descrita como una base de datos relacional , decida si la interpretación es un modelo de la fórmula.

Este problema pertenece a la clase de circuitos AC ^0. Es tratable al imponer algunas restricciones a la estructura de entrada: por ejemplo, exigir que tenga un ancho de árbol acotado por una constante (lo que implica, de forma más general, la tratabilidad de la verificación de modelos para la lógica monádica de segundo orden ), acotar el grado de cada elemento del dominio y condiciones más generales como la expansión acotada , la expansión localmente acotada y las estructuras no densas en ninguna parte. ^{[ 21 ]} Estos resultados se han extendido a la tarea de enumerar todas las soluciones a una fórmula de primer orden con variables libres.

Aquí hay una lista de herramientas importantes para la verificación de modelos:

• Afra: un verificador de modelos para Rebeca , que es un lenguaje basado en actores para modelar sistemas concurrentes y reactivos.
• Aleación (Analizador de aleaciones)
• BLAST (Herramienta de verificación de software de abstracción perezosa de Berkeley)
• CADP (Construction and Analysis of Distributed Processes) es un conjunto de herramientas para el diseño de protocolos de comunicación y sistemas distribuidos.
• CPAchecker : un verificador de modelos de software de código abierto para programas en C, basado en el marco de trabajo CPA.
• ECLAIR : una plataforma para el análisis, verificación, prueba y transformación automáticos de programas C y C++.
• FDR2 : un verificador de modelos para comprobar sistemas en tiempo real modelados y especificados como procesos CSP.
• FizzBee : una alternativa más fácil de usar que TLA+, que utiliza un lenguaje de especificación similar a Python y que cuenta con modelado de comportamiento como TLA+ y modelado probabilístico como PRISM.
• Verificador de nivel de código ISP para programas MPI
• Java Pathfinder : un verificador de modelos de código abierto para programas Java.
• Libdmc : un marco de trabajo para la verificación de modelos distribuidos
• Conjunto de herramientas mCRL2 , licencia de software Boost , basado en ACP
• NuSMV : un nuevo verificador de modelos simbólicos
• PAT : un simulador mejorado, un verificador de modelos y un verificador de refinamiento para sistemas concurrentes y en tiempo real.
• Prisma : un verificador de modelos simbólicos probabilísticos
• Roméo : un entorno de herramientas integrado para el modelado, la simulación y la verificación de sistemas en tiempo real modelados como redes de Petri paramétricas, de tiempo y de cronómetro.
• SPIN : una herramienta general para verificar la corrección de modelos de software distribuidos de forma rigurosa y mayoritariamente automatizada.
• Storm : ^{[ 22 ]} Un verificador de modelos para sistemas probabilísticos.
• TAPAs : una herramienta para el análisis del álgebra de procesos
• TAPAAL : un entorno de herramientas integrado para el modelado, validación y verificación de redes de Petri de arco temporizado.
• Comprobador de modelos TLA+ por Leslie Lamport
• UPPAAL : un entorno de herramientas integrado para el modelado, validación y verificación de sistemas en tiempo real modelados como redes de autómatas temporizados.
• Zing ^{[ 23 ]} es una herramienta experimental de Microsoft para validar modelos de estado de software en varios niveles: descripciones de protocolos de alto nivel, especificaciones de flujo de trabajo, servicios web, controladores de dispositivos y protocolos en el núcleo del sistema operativo. Actualmente, Zing se utiliza para desarrollar controladores para Windows.