Comprobación de modelos

Campo de la informática

El software de control de ascensores se puede comprobar mediante modelos para verificar tanto las propiedades de seguridad, como "La cabina nunca se mueve con la puerta abierta" , ^[1] y las propiedades de actividad, como "Siempre que se presione el botón de llamada del piso ⁿ , la cabina eventualmente se detendrá en el piso n ^y abrirá la puerta" .

En informática , la comprobación de modelos o comprobación de propiedades es un método para comprobar si un modelo de estados finitos de un sistema cumple 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 actividad (como evitar bloqueos activos ) así como requisitos de seguridad (como evitar estados que representen un fallo del sistema ).

Para resolver un problema de este tipo de manera algorítmica , tanto el modelo del sistema como su especificación se formulan en un lenguaje matemático preciso. Para ello, el problema se formula como una tarea de 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 muchos tipos de estructuras. Un problema simple de comprobación de modelos consiste en verificar si una fórmula de la lógica proposicional se satisface con una estructura dada.

Descripción general

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 que no son necesarios en la especificación de nivel superior. No hay necesidad de 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 verificar modelos de diseños de hardware y software donde la especificación está dada por una fórmula de lógica temporal . El trabajo pionero en la especificación de la lógica temporal fue realizado por Amir Pnueli , quien recibió el premio Turing de 1996 por "trabajo seminal introduciendo 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 seminal que fundó y desarrolló el campo de la verificación de modelos. ^{[8] [9]}

La comprobación de modelos se aplica con mayor frecuencia a los diseños de hardware. En el caso del software, debido a la indecidibilidad (véase 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 el hardware de sistemas embebidos , es posible validar una especificación entregada, por ejemplo, por medio de diagramas de actividad UML ^{[10] o} redes de Petri interpretadas por control . ^[11]

La estructura se proporciona generalmente como una descripción del código fuente en un lenguaje de descripción de hardware industrial o un lenguaje de propósito especial. Un programa de este tipo corresponde a una máquina de estados finitos (FSM), es decir, un gráfico dirigido que consta de nodos (o vértices ) y aristas . Un conjunto de proposiciones atómicas se asocia con cada nodo, que normalmente indica 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 mantienen en un punto de ejecución. ^[12]

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

Comprobación del modelo simbólico

En lugar de enumerar los estados alcanzables de uno en uno, el espacio de estados a veces se puede recorrer de manera más eficiente considerando una gran cantidad 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 binaria (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 utilizaban BDD . Después del éxito de la satisfacibilidad proposicional en la solución del problema de planificación en inteligencia artificial (véase satplan ) en 1996, el mismo enfoque se generalizó a la comprobación de modelos para lógica temporal lineal (LTL): el problema de planificación corresponde a la comprobación de modelos para propiedades de seguridad. Este método se conoce como comprobación de modelos acotados. ^[13] El éxito de los solucionadores de satisfacibilidad booleanos en la comprobación de modelos acotados condujo al uso generalizado de solucionadores de satisfacibilidad en la comprobación de modelos simbólicos. ^[14]

Ejemplo

Un ejemplo de un requisito de este tipo es el siguiente: 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 "Patrones en la especificación de propiedades para la verificación de estados finitos" traducen este requisito en la siguiente fórmula LTL: ^[15]

${\displaystyle {\begin{aligned}\Box {\Big (}({\texttt {call}}\land \Diamond {\texttt {open}})\to &{\big (}(\lnot {\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor ((\lnot {\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (\lnot {\texttt {atfloor}}~{\mathcal {U}}~{\texttt {open}})))))))){\big )}{\Big )}\end{aligned}}}$

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". ${\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 un problema de explosión combinatoria del espacio de estados, conocido comúnmente como el problema de 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 gráfico de las máquinas de estados finitos (FSM); en cambio, representan el gráfico de manera implícita utilizando una fórmula en lógica proposicional cuantificada. El uso de diagramas de decisión binaria (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 desenrollan la FSM para una cantidad fija de pasos, y verifican si una violación de propiedad puede ocurrir en o menos pasos. Esto generalmente implica codificar el modelo restringido como una instancia de SAT . El proceso se puede repetir con valores cada vez mayores de hasta que se hayan descartado todas las posibles violaciones (cf. Búsqueda en profundidad con profundización iterativa ). ${\displaystyle k}$ ${\displaystyle k}$ ${\displaystyle k}$
3. La abstracción intenta demostrar las propiedades de un sistema simplificándolo primero. El sistema simplificado normalmente 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 demostradas en la abstracción sean 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; tal 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 burda (es decir, imprecisa) y la refina iterativamente. Cuando se encuentra una violación (es decir, un contraejemplo ), la herramienta la analiza para determinar su viabilidad (es decir, ¿la violación es genuina o el resultado de una abstracción incompleta?). Si la violación es factible, se informa al usuario. Si no lo es, se utiliza la prueba de inviabilidad 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 formas limitadas y en tiempo real de sistemas híbridos .

Lógica de primer orden

La comprobación de modelos también se estudia en el campo de la teoría de la complejidad computacional . En concreto, 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 circuito AC 0 . Es manejable al imponer algunas restricciones a la estructura de entrada: por ejemplo, requiriendo que tenga un ancho de árbol limitado por una constante (lo que implica de manera más general la manejabilidad de la verificación de modelos para lógica monádica de segundo orden ), limitando el grado de cada elemento del dominio y condiciones más generales como expansión limitada , expansión localmente limitada y estructuras 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. ^{[ cita requerida ]}

Herramientas

A continuación se muestra una lista de herramientas importantes de 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 diferida 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 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 verificador 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 , basada 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
• Prism : un verificador de modelos simbólicos probabilísticos
• Roméo : un entorno de herramientas integrado para modelar, simular y verificar 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 manera 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 modelar, validar y verificar redes de Petri de arco temporizado
• Comprobador de modelos TLA+ de Leslie Lamport
• UPPAAL : un entorno de herramientas integrado para modelar, validar y verificar sistemas en tiempo real modelados como redes de autómatas temporizados
• Zing ^[23] – 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. Zing se utiliza actualmente para desarrollar controladores para Windows.

Véase también

• Interpretación abstracta
• Demostración automática de teoremas
• Diagrama de decisión binaria
• Autómata Büchi
• Lógica del árbol de cálculo
• Refinamiento de abstracción guiado por contraejemplos
• Verificación formal
• Lógica temporal lineal
• Lista de herramientas de verificación de modelos
• Reducción parcial de pedidos
• Análisis de programas (informática)
• Análisis de código estático

Referencias

1. Para mayor comodidad, las propiedades de ejemplo se parafrasean aquí en lenguaje natural. Los verificadores de modelos requieren que se expresen en alguna lógica formal, como LTL .
2. Lam K., William (2005). "Capítulo 1.1: ¿Qué es la verificación de diseño?". Verificación de diseño de hardware: simulación y enfoques basados ​​en métodos formales . Consultado el 12 de diciembre de 2012 .
3. "Amir Pnueli - Ganador del premio AM Turing".
4. Allen Emerson, E.; Clarke, Edmund M. (1980), "Caracterización de las propiedades de corrección de programas paralelos utilizando puntos fijos", Automata, Languages ​​and Programming , Lecture Notes in Computer Science, vol. 85, págs. 169-181, doi :10.1007/3-540-10003-2_69, ISBN 978-3-540-10003-4
5. 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". Logic of Programs 1981: 52-71.
6. Clarke, EM; Emerson, EA; Sistla, AP (1986), "Verificación automática de sistemas concurrentes de estados finitos utilizando especificaciones de lógica temporal", ACM Transactions on Programming Languages ​​and Systems , 8 (2): 244, doi : 10.1145/5397.5399 , S2CID  52853200
7. Queille, JP; Sifakis, J. (1982), "Especificación y verificación de sistemas concurrentes en CESAR", Simposio Internacional sobre Programación , Lecture Notes in Computer Science, vol. 137, págs. 337–351, doi :10.1007/3-540-11494-7_22, ISBN 978-3-540-11494-9
8. "Comunicado de prensa: el premio Turing de la ACM 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 .
9. USACM: Se anuncian los ganadores del premio Turing 2007
10. 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 sistemas inteligentes y computación. Vol. 286. págs. 233–242. doi :10.1007/978-3-319-07013-1_22. ISBN 978-3-319-07012-4.
11. I. Grobelna, "Verificación formal de la especificación de un controlador lógico integrado con deducción por computadora en lógica temporal", Przeglad Elektrotechniczny, vol. 87, número 12a, págs. 47-50, 2011
12. Este artículo se basa en material tomado de Model+checking en el Diccionario gratuito en línea de computación antes del 1 de noviembre de 2008 e incorporado bajo los términos de "relicencia" del GFDL , versión 1.3 o posterior.
13. Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "Comprobación de modelos acotados mediante resolución de satisfacibilidad". Métodos formales en diseño de sistemas . 19 : 7–34. doi :10.1023/A:1011276507260. S2CID  2484208.
14. Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Solucionadores de satisfacibilidad booleana y sus aplicaciones en la verificación de modelos". Actas del IEEE . 103 (11): 2021–2035. doi :10.1109/JPROC.2015.2455034. S2CID  10190144.
15. Dwyer, M.; Avrunin, G.; Corbett, J. (mayo de 1999). "Patrones en especificaciones de propiedades para verificación de estados finitos". Patrones en especificaciones de propiedades para verificación de estados finitos. Actas de la 21.ª conferencia internacional sobre ingeniería de software. págs. 411–420. doi :10.1145/302405.302672. ISBN 1581130740.
16. * Verificación de modelos simbólicos , Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5 , también en línea Archivado el 2 de junio de 2007 en Wayback Machine . 
17. Coudert, O.; Madre, JC (1990). "Un marco unificado para la verificación formal de circuitos secuenciales" (PDF) . Conferencia internacional sobre diseño asistido por computadora . IEEE Comput. Soc. Press: 126–129. doi :10.1109/ICCAD.1990.129859. ISBN . 978-0-8186-2055-3.
18. "CUDD: Paquete de diagrama de decisión de CU".
19. "BuDDy – Un paquete de diagrama de decisión binario".
20. Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut (2000), "Refinamiento de abstracción guiado por contraejemplos", Verificación asistida por computadora (PDF) , Lecture Notes in Computer Science, vol. 1855, págs. 154–169, doi : 10.1007/10722167_15 , ISBN 978-3-540-67770-3
21. Dawar, A; Kreutzer, S (2009). "Complejidad parametrizada de la lógica de primer orden" (PDF) . ECCC . S2CID  5856640. Archivado desde el original (PDF) el 2019-03-03.
22. Comprobador de modelos de tormentas
23. Zumbido

Lectura adicional

• Peled, Dorón A .; Pelliccione, Patrizio; Spoletini, Paola (2009). "Comprobación de modelos". Enciclopedia Wiley de Ingeniería y Ciencias de la Computación . págs. 1904-1920. doi : 10.1002/9780470050118.ecse247. ISBN 978-0-470-05011-8. Número de identificación del sujeto  5371327.
• Clarke, Edmund M. ; Grumberg, Orna ; Peled, Doron A. (1999). Verificación de modelos . MIT Press . ISBN 0-262-03270-8.
• Berard, B.; Bidoit, M.; Finkel, A.; Laroussinie, F.; Petit, A.; Petrucci, L.; Schnoebelen, P. Verificación de sistemas y software: técnicas y herramientas de verificación de modelos . ISBN 3-540-41523-8.
• Huth, Michael; Ryan, Mark (2004). Lógica en informática: modelado y razonamiento sobre sistemas . Cambridge University Press .
• Holzmann, Gerard J. El verificador de modelos de espín: manual de referencia y de introducción. Addison-Wesley. ISBN 0-321-22862-6.
• Bradfield, Julian; Stirling, Colin (2001). "Lógicas modales y cálculos mu: una introducción". Manual de álgebra de procesos . Elsevier. págs. 293–330. doi :10.1016/B978-044482830-9/50022-9. ISBN 978-0-444-82830-9.. JA Bergstra, A. Ponse y SA Smolka, editores." ().
• "Patrones de especificación". Laboratorio SAnToS, Universidad Estatal de Kansas. Archivado desde el original el 19 de julio de 2011.
• "Mapeo de patrones de propiedades para RAFMC". CADP: Construcción y análisis de procesos distribuidos . 2019.
• Mateescu, Radu; Sighireanu, Mihaela (2003). "Verificación eficiente de modelos sobre la marcha para cálculos Mu regulares sin alternancia" (PDF) . Science of Computer Programming . 46 (3): 255–281. doi :10.1016/S0167-6423(02)00094-1. S2CID  10942856.
• Müller-Olm, M.; Schmidt, DA; Steffen, B. (1999). "Verificación de modelos: una introducción didáctica". Análisis estático: 6.º simposio internacional, SAS'99, Venecia, Italia, 22-24 de septiembre de 1999, Actas . Vol. 1694. LNCS: Springer. págs. 330–354. CiteSeerX  10.1.1.96.3011 . doi :10.1007/3-540-48294-6_22. ISBN . 978-3-540-48294-9.
• Baier, C. ; Katoen, J. (2008). Principios de verificación de modelos . MIT Press. ISBN 978-0-262-30403-0.
• Clarke, EM (2008). "El nacimiento de la comprobación de modelos". 25 años de comprobación de modelos . Apuntes de clase en informática. Vol. 5000. págs. 1–26. doi :10.1007/978-3-540-69850-0_1. ISBN 978-3-540-69849-4.
• Emerson, E. Allen (2008). "El comienzo de la verificación de modelos: una perspectiva personal". En Grumberg, Orna; Veith, Helmut (eds.). 25 años de verificación de modelos: historia, logros, perspectivas. LNCS. Vol. 5000. 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)