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.
Descripció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. [2]
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". [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 2007 por su trabajo fundamental en la fundación y desarrollo del campo de la verificación de modelos. [8] [9]
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 siempre dar 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 [10] o redes de Petri interpretadas de control . [11]
La estructura generalmente se da 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 , decide si . Sies finito, como lo es en el hardware, la verificación del modelo se reduce a una búsqueda gráfica .
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. [12] El éxito de los solucionadores de satisfacibilidad booleanos en la verificación de modelos acotados condujo al uso generalizado de solucionadores de satisfacibilidad en la verificación de modelos simbólicos. [13]
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 a la siguiente fórmula LTL: [14]
Aquí, debe leerse como "siempre", como "eventualmente", como "hasta" y los demás símbolos son símbolos lógicos estándar, para "o", para "y" y para no".
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 hizo popular por el trabajo de Ken McMillan [15] y el desarrollo de bibliotecas de manipulación de BDD de código abierto como CUDD [16] y BuDDy. [17]
- Los algoritmos de verificación de modelos limitados desenrollan el FSM para un número fijo de pasos, y verifique si puede ocurrir una infracción a la propiedad en o menos pasos. Por lo general, esto implica codificar el modelo restringido como una instancia de SAT . El proceso se puede repetir con valores cada vez mayores dehasta que se hayan descartado todas las posibles infracciones (cf. Profundización iterativa de búsqueda en profundidad primero ).
- 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 de 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í, se utiliza la prueba de inviabilidad para refinar la abstracción y la verificación comienza de nuevo. [18]
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 0 . 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. [19] Estos resultados se han extendido a la tarea de enumerar todas las soluciones a una fórmula de primer orden con variables libres. [ cita requerida ]
Herramientas
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 [20] : 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
- Lista de herramientas de verificación de modelos
- Diagrama de decisión binaria
- Autómata Büchi
- Lógica del árbol de cálculo
- Verificación formal
- Lógica temporal lineal
- Reducción parcial de pedidos
- Análisis de programas (informática)
- Interpretación abstracta
- Demostración automatizada de teoremas
- Análisis de código estático
Referencias
Citas
- ^ Por conveniencia, aquí se parafrasean las propiedades de ejemplo en lenguaje natural. Los verificadores de modelos requieren que se expresen en alguna lógica formal, como LTL .
- ^ Lam K., William (2005). "Capítulo 1.1: ¿Qué es la verificación de diseño?" . Verificación del diseño de hardware: simulación y enfoques basados en métodos formales . Consultado el 12 de diciembre de 2012 .
- ^ "Amir Pnueli - AM Turing Award Laureate" .
- ^ Allen Emerson, E .; Clarke, Edmund M. (1980), "Caracterización de las propiedades de corrección de programas paralelos utilizando puntos de referencia", Autómatas, lenguajes y programación , Lecture Notes in Computer Science, 85 : 169-181, doi : 10.1007 / 3-540-10003-2_69 , ISBN 978-3-540-10003-4
- ^ Edmund M. Clarke, E. Allen Emerson: "Diseño y síntesis de esqueletos de sincronización utilizando lógica temporal de tiempo de ramificación" . Lógica de programas 1981: 52-71.
- ^ Clarke, EM; Emerson, EA; Sistla, AP (1986), "Verificación automática de sistemas concurrentes de estado finito usando especificaciones lógicas temporales", Transacciones ACM en lenguajes y sistemas de programación , 8 (2): 244, doi : 10.1145 / 5397.5399
- ^ Queille, JP; Sifakis, J. (1982), "Especificación y verificación de sistemas concurrentes en CESAR", Simposio internacional de programación , Lecture Notes in Computer Science, 137 : 337–351, doi : 10.1007 / 3-540-11494-7_22 , ISBN 978-3-540-11494-9
- ^ "Comunicado de prensa: Premio ACM Turing honra a los fundadores de la tecnología de verificación automática" . Archivado desde el original el 28 de diciembre de 2008 . Consultado el 6 de enero de 2009 .
- ^ USACM : Se anunciaron los ganadores del premio Turing 2007
- ^ Grobelna, Iwona; Grobelny, Michał; Adamski, Marian (2014). "Verificación de modelos de diagramas de actividad UML en el diseño de controladores lógicos". Actas de la Novena Conferencia Internacional sobre Confiabilidad y Sistemas Complejos DepCoS-RELCOMEX. 30 de junio - 4 de julio de 2014, Brunów, Polonia . Avances en Computación y Sistemas Inteligentes. 286 . págs. 233–242. doi : 10.1007 / 978-3-319-07013-1_22 . ISBN 978-3-319-07012-4.
- ^ I. Grobelna, " Verificación formal de la especificación del controlador lógico integrado con deducción por computadora en lógica temporal ", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47-50, 2011
- ^ Clarke, E .; Biere, A .; Raimi, R .; Zhu, Y. (2001). "Comprobación del modelo acotado mediante resolución de satisfacción". Métodos formales en el diseño de sistemas . 19 : 7-34. doi : 10.1023 / A: 1011276507260 .
- ^ Vizel, Y .; Weissenbacher, G .; Malik, S. (2015). "Solucionadores de satisfacción booleana y sus aplicaciones en la comprobación de modelos". Actas del IEEE . 103 (11): 2021-2035. doi : 10.1109 / JPROC.2015.2455034 .
- ^ Dwyer, M .; Avruin, G .; Corbett, J. (marzo de 1998). Ardis, M. (ed.). Patrones en la especificación de propiedades para la verificación de estados finitos (PDF) . Actas del segundo taller sobre métodos formales en la práctica del software. págs. 7–15.
- ^ * Comprobación del modelo simbólico , Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5 , también en línea Archivado 2007-06-02 en Wayback Machine .
- ^ "CUDD: Paquete de diagrama de decisiones de CU" .
- ^ "BuDDy - un paquete de diagrama de decisión binaria" .
- ^ Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut (2000), "Refinamiento de abstracción guiado por contraejemplos" (PDF) , Verificación asistida por computadora , Notas de conferencias en Ciencias de la computación, 1855 : 154-169, doi : 10.1007 / 10722167_15 , ISBN 978-3-540-67770-3
- ^ Dawar, A; Kreutzer, S (2009). "Complejidad parametrizada de la lógica de primer orden" (PDF) . ECCC . S2CID 5856640 . Archivado desde el original (PDF) el 3 de marzo de 2019.
- ^ Zing
Fuentes
- Este artículo se basa en material extraído del Diccionario gratuito de informática en línea antes del 1 de noviembre de 2008 e incorporado bajo los términos de "renovación de licencias" de la GFDL , versión 1.3 o posterior.
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)