Comprobación del modelo - Model checking

El software de control de ascensores se puede verificar en el modelo para verificar tanto las propiedades de seguridad, como "La cabina nunca se mueve con la puerta abierta" , y las propiedades de vitalidad, como "Siempre que se presione el botón de llamada del n- ^ésimo piso , la cabina finalmente se detendrá en el n. ^º piso y abrir la puerta" .

En ciencias de la computación , la verificación de modelos o verificación de propiedades es un método para verificar si un modelo de estado finito de un sistema cumple con una especificación dada (también conocida como corrección ). Esto generalmente se asocia con sistemas de hardware o software , donde la especificación contiene requisitos de vida (como evitar el bloqueo en vivo ), así como requisitos de seguridad (como evitar estados que representan un bloqueo del sistema ).

Para resolver este problema 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 en lógica , es decir, verificar 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 simple de verificación de modelos consiste en verificar si una fórmula en la lógica proposicional es satisfecha por una estructura dada.

Visión general

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

Se ha desarrollado una clase importante de métodos de verificación de modelos para verificar modelos de diseños de hardware y software donde la especificación viene dada por una fórmula lógica temporal . Amir Pnueli , quien recibió el premio Turing en 1996, realizó un trabajo pionero en la especificación de la lógica temporal por su "trabajo fundamental en la introducción de la lógica temporal en la ciencia de la computación". La verificación de modelos comenzó con el trabajo pionero de EM Clarke , EA Emerson , por JP Queille y J. Sifakis . Clarke, Emerson y Sifakis compartieron el premio Turing 2007 por su trabajo fundamental en la fundación y desarrollo del campo de la verificación de modelos.

La verificación de modelos se aplica con mayor frecuencia a los diseños de hardware. Para el software, debido a la indecidibilidad (ver teoría de la computabilidad ), el enfoque no puede ser completamente algorítmico, aplicarse a todos los sistemas y dar siempre una respuesta; en el caso general, puede fallar en probar o refutar una propiedad dada. En hardware de sistemas embebidos , es posible validar una especificación entregada, es decir, mediante diagramas de actividad UML o redes de Petri de control interpretadas .

La estructura generalmente se proporciona como una descripción de código fuente en un lenguaje de descripción de hardware industrial o un lenguaje de propósito especial. Dicho programa corresponde a una máquina de estados finitos (FSM), es decir, un grafo dirigido que consta de nodos (o vértices ) y aristas . Un conjunto de proposiciones atómicas se asocia con cada nodo, que típicamente indica qué elementos de memoria son uno. Los nodos representan estados de un sistema, los bordes representan posibles transiciones que pueden alterar el estado, mientras que las proposiciones atómicas representan las propiedades básicas que se mantienen en un punto de ejecución.

Formalmente, el problema se puede plantear de la siguiente manera: dada una propiedad deseada, expresada como una fórmula lógica temporal , y una estructura con estado inicial , decida si . Si es finito, como lo es en el hardware, la verificación del modelo se reduce a una búsqueda gráfica . ${\ Displaystyle p}$ ${\ Displaystyle M}$ ${\ Displaystyle s}$ ${\ Displaystyle M, s \ modelos p}$ ${\ Displaystyle M}$

Comprobación del modelo simbólico

En lugar de enumerar los estados alcanzables uno a la vez, el espacio de estados a veces se puede atravesar de manera más eficiente al considerar un gran número de estados en un solo paso. Cuando tal 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 binaria (BDD) u otras estructuras de datos relacionadas, el método de verificación del modelo es simbólico .

Históricamente, los primeros métodos simbólicos utilizaron BDD . Después del éxito de la satisfacibilidad proposicional en la resolución del problema de planificación en inteligencia artificial (ver satplan ) en 1996, el mismo enfoque se generalizó a la verificación de modelos para la lógica temporal lineal (LTL): el problema de planificación corresponde a la verificación del modelo para las propiedades de seguridad. Este método se conoce como verificación de modelo acotado. El éxito de los solucionadores de satisfacibilidad booleanos en la verificación de modelos acotados llevó al uso generalizado de solucionadores de satisfacibilidad en la verificación de modelos simbólicos.

Ejemplo

Un ejemplo de un requisito del sistema de este tipo: entre el momento en que se llama a un ascensor en un piso y el momento en que abre sus puertas en ese piso, el ascensor puede llegar a ese piso como máximo dos veces . Los autores de "Patterns in Property Specification for Finite-State Verification" traducen este requisito en la siguiente fórmula LTL:

{\ displaystyle {\ begin {alineado} \ Box ((llamar \ lor \ Diamond open) \ to & ((\ lnot atfloor \ lor \ l not open) ~ {\ mathcal {U}} \\ & (open \ lor ( (en el piso \ terreno \ lno abierto) ~ {\ mathcal {U}} \\ & (abierto \ lor ((\ no en el piso \ terreno \ lno abierto) ~ {\ mathcal {U}} \\ & (abierto \ lor ( (en el piso \ tierra \ lno abierto) ~ {\ mathcal {U}} \\ & (abierto \ lor (\ lno en el piso ~ {\ mathcal {U}} ~ abierto))))))))))) \ end {alineado}}}

Aquí, debe leerse como "siempre", como "eventualmente", como "hasta" y los otros símbolos son símbolos lógicos estándar, para "o", para "y" y para "no". ${\ Displaystyle \ Box}$ ${\ Displaystyle \ Diamond}$ ${\ Displaystyle {\ mathcal {U}}}$ ${\ Displaystyle \ lor}$ ${\ Displaystyle \ land}$ ${\ Displaystyle \ lnot}$

Técnicas

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. Hay varios enfoques para combatir este problema.

Los algoritmos simbólicos evitan construir explícitamente el gráfico para las máquinas de estados finitos (FSM); en cambio, representan el gráfico implícitamente usando 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 y al desarrollo de bibliotecas de manipulación de BDD de código abierto como CUDD y BuDDy.
Los algoritmos de verificación de modelos limitados desenrollan el FSM para un número fijo de pasos y verifican si una infracción de propiedad puede ocurrir en o menos pasos. Por lo general, esto implica codificar el modelo restringido como una instancia de SAT . El proceso puede repetirse con valores cada vez mayores de hasta que se hayan descartado todas las posibles infracciones (cf. Búsqueda iterativa de profundización en profundidad primero ). ${\ Displaystyle k}$ ${\ Displaystyle k}$ ${\ Displaystyle k}$
La abstracción intenta probar las 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. Generalmente, se requiere que la abstracción sea sólida (las propiedades probadas en la abstracción son verdaderas del 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 solo considerar las variables booleanas y el flujo de control del programa; tal abstracción, aunque pueda parecer burda, puede, de hecho, ser suficiente para probar, por ejemplo, las propiedades de la exclusión mutua .
El refinamiento de abstracción guiada de contraejemplo (CEGAR) comienza a verificar con una abstracción burda (es decir, imprecisa) y la refina iterativamente. Cuando se encuentra una infracción (es decir, un contraejemplo ), la herramienta la analiza para determinar su viabilidad (es decir, ¿la infracción es genuina o el resultado de una abstracción incompleta?). Si la infracción es factible, se informa al usuario. Si no es así, la prueba de inviabilidad se usa para refinar la abstracción y la verificación comienza de nuevo.

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 tratar formas limitadas y en tiempo real de sistemas híbridos .

Lógica de primer orden

La verificación de modelos también se estudia en el campo de la teoría de la complejidad computacional . Específicamente, una fórmula lógica de primer orden se fija 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 está en la clase de circuito AC ⁰ . Es manejable cuando se imponen algunas restricciones a la estructura de entrada: por ejemplo, requiriendo que tenga un ancho de árbol limitado por una constante (que más generalmente implica la tractabilidad de la verificación del modelo para la lógica monádica de segundo orden ), delimitando el grado de cada elemento del dominio, y condiciones más generales, como expansión limitada, expansión limitada localmente y estructuras densas en ninguna parte. Estos resultados se han extendido a la tarea de enumerar todas las soluciones a una fórmula de primer orden con variables libres.

Instrumentos

A continuación, se muestra una lista de importantes herramientas de verificación de modelos:

Aleación (analizador de aleaciones)
BLAST (Herramienta de verificación del software de abstracción perezosa de Berkeley)
CADP (Construcción y Análisis de Procesos Distribuidos) una caja 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 C, basado en el marco de 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 verificar sistemas en tiempo real modelados y especificados como procesos CSP
Verificador de nivel de código ISP para programas MPI
Java Pathfinder : un comprobador de modelos de código abierto para programas Java
Libdmc : un marco 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, verificador de modelos y 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, simulación y 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 los modelos de software distribuidos de una manera rigurosa y en su mayoría automatizada
TAPA : 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 + de 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: herramienta experimental de Microsoft para validar modelos de software de estado 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.

Ver también

Referencias

Otras lecturas

Verificación de modelos , Doron A. Peled , Patrizio Pelliccione, Paola Spoletini, Enciclopedia Wiley de Ciencias de la Computación e Ingeniería, 2009.
Model Checking , Edmund M. Clarke , Orna Grumberg y Doron A. Peled, MIT Press , 1999, ISBN 0-262-03270-8 .
Verificación de sistemas y software: técnicas y herramientas de verificación de modelos , B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, ISBN 3-540-41523-8
Lógica en Ciencias de la Computación: Modelado y Razonamiento de Sistemas , Michael Huth y Mark Ryan, Cambridge University Press , 2004. doi : 10.2277 / 052154310X .
The Spin Model Checker: Primer y manual de referencia , Gerard J. Holzmann , Addison-Wesley, ISBN 0-321-22862-6 .
Julian Bradfield y Colin Stirling, lógicas modales y mu-calculi, Inf.ed.ac.uk
Patrones de especificación KSU.edu
Asignaciones de patrones de propiedad para RAFMC Inria.fr
Radu Mateescu y Mihaela Sighireanu Comprobación de modelos sobre la marcha eficiente para el cálculo de Mu regular sin alternancia , página 6, Science of Computer Programming 46 (3): 255–281, 2003
Müller-Olm, M., Schmidt, DA y Steffen, B. Verificación de modelos: una introducción tutorial. Proc. Sexto Simposio de análisis estático, G. File y A. Cortesi, eds., Springer LNCS 1694, 1999, págs. 330–354.
Baier, C. , Katoen, J .: Principios de verificación de modelos. 2008.
EM Clarke : "El nacimiento de la verificación de modelos" doi : 10.1007 / 978-3-540-69850-0_1
E. Allen Emerson (2008). "El comienzo de la comprobación de modelos: una perspectiva personal". En Orna Grumberg; Helmut Veith (eds.). 25 años de verificación de modelos: historia, logros, perspectivas . LNCS. 5000 . Heidelberg: Springer. págs. 27–45. doi : 10.1007 / 978-3-540-69850-0_2 . ISBN 978-3-540-69849-4. (esta es también una muy buena introducción y descripción general de la verificación de modelos)

Languages

In other projects