Lista de herramientas de verificación de modelos

Este artículo enumera las herramientas de verificación de modelos y ofrece una descripción general de la funcionalidad de cada una.

Descripción general de algunas herramientas de verificación de modelos

La siguiente tabla incluye verificadores de modelos que tienen

1. un sitio web desde el que se puede descargar,
2. una licencia declarada,
3. una descripción publicada en literatura archivada, y
4. Un artículo de Wikipedia que lo describe.

En la siguiente tabla se utilizan las siguientes abreviaturas:

• Equivalencias:
  • SB: Bisimulación fuerte
  • WB: Bisimulación débil
  • BB: Bisimulación de ramificación
  • STE: Equivalencia de traza fuerte
  • WTE: Equivalencia de trazas débiles
  • yo: Equivalencia de mayo
  • YO: Debe Equivalencia
  • OE: Equivalencia observacional
  • SE: Equivalencia de seguridad
  • t*E: tau*.a Equivalencia
• Licencia del software:
  • FUSC: Gratuito bajo condiciones específicas (por ejemplo, gratuito para fines académicos)

Lenguajes de modelado

• CCSP: cálculo de procesos obtenido a partir de CCS mediante la incorporación de algunos operadores de CSP . Está definido por Olderog ^[1] y por van Glabbeek/Vaandrager. ^[2]
• CSP : Comunicación de procesos secuenciales; lenguaje formal para describir patrones de interacción en sistemas concurrentes. FDR2 es una herramienta de comprobación de refinamiento para CSP que compara dos modelos para comprobar su compatibilidad.
• Lenguaje de entrada DVE: un sistema se describe como una red de máquinas de estados finitos extendidas que se comunican a través de variables compartidas y canales sin búfer. No contiene soporte para canales con búfer ni para verificar el tipo de mensaje que se recibirá sin realizar la recepción propiamente dicha.
• FC2: (Common Format V2) Representación ASCII a nivel de máquina para redes sincronizadas (jerárquicas) de autómatas. Definida por la Acción de Investigación Básica Esprit CONCUR, 1992. Utilizada como formato de entrada e intercambio por varias herramientas de verificación, principalmente en el área de álgebras de procesos.
• FSP: Lenguaje de Procesos de Estados Finitos definido en el Imperial College.
• Java : Lenguaje de programación orientado a objetos.
• LNT: LOTOS New Technology; un lenguaje de especificación inspirado en cálculos de procesos, lenguajes de programación funcional y lenguajes de programación imperativos; LNT fue diseñado como un reemplazo moderno para LOTOS y E-LOTOS .
• LOTOS : Lenguaje de especificación de ordenamiento temporal (norma ISO 8807); lenguaje de especificación formal basado en el ordenamiento temporal utilizado para la especificación de protocolos en las normas ISO OSI.
• mCRL2 : un lenguaje de especificación para describir sistemas de eventos discretos concurrentes.
• Murφ : Comandos protegidos y un modelo de concurrencia entrelazado y asincrónico, con toda la sincronización y comunicación realizada a través de variables globales.
• PEPA : Álgebra de procesos de evaluación del desempeño; es un álgebra de procesos estocásticos diseñada para modelar sistemas informáticos y de comunicación.
• MC simple: formatos de archivos de texto simples utilizados en MRMC y PRISM.
• Promela : Metalenguaje de procesos o protocolos; es un lenguaje de modelado de verificación. El lenguaje permite la creación dinámica de procesos concurrentes para modelar, por ejemplo, sistemas distribuidos.
• TLA+ : Lenguaje de especificación de propósito general basado en la lógica temporal de acciones, utilizado originalmente para sistemas distribuidos y concurrentes. El lenguaje para las especificaciones y sus propiedades es el mismo.

Propiedades del idioma

• AFMC: μ-cálculo modal libre de alternancia .
• Afirmaciones : Declaraciones de afirmación imperativas.
• CSL: Lógica Estocástica Continua, caracteriza la bisimulación de procesos de Markov en tiempo continuo.
• CSRL: Lógica de recompensa estocástica continua; una lógica para especificar medidas sobre CTMC extendidas con una estructura de recompensa (los llamados modelos de recompensa de Markov).
• CTL : Lógica de árbol de cálculo; una lógica de tiempo ramificado, lo que significa que su modelo de tiempo es una estructura tipo árbol en la que el futuro no está determinado; hay diferentes caminos en el futuro, cualquiera de los cuales podría ser un camino real que se realice.
• Invariantes : Predicados sobre un estado del sistema.
• LTL : Lógica temporal lineal; una lógica temporal modal con modalidades referentes al tiempo.
• MCL: Lenguaje de verificación de modelos; μ-cálculo modal libre de alternancia extendido con expresiones regulares fáciles de usar y construcciones de paso de valores; subsume CTL y LTL .
• mCRL2 mu-calculus: μ-cálculo modal proposicional de Kozen (excluyendo proposiciones atómicas), ampliado con: procesos dependientes de datos, cuantificación sobre tipos de datos, acciones múltiples, tiempo y fórmulas regulares.
• PCTL : CTL probabilístico ; una extensión de CTL que permite la cuantificación probabilística de las propiedades descritas.
• PLTL: Lógica temporal lineal probabilística.
• PRCTL: Lógica de árbol de cálculo de recompensa probabilística; extiende PCTL con propiedades limitadas por recompensa.
• PSL : Lenguaje de especificación de propiedades
• SVA: subconjunto del lenguaje de aserción de estándares SystemVerilog , estandarizado como IEEE 1800
• XTL: lenguaje temporal extendido; un lenguaje específico de dominio para implementar rápidamente verificadores de modelos basados ​​en acciones, de estado explícito y de paso de valores.

Comparación de herramientas de verificación de modelos

Publicaciones científicas

Existen algunos artículos que comparan sistemáticamente varios verificadores de modelos en un caso de estudio común. La comparación generalmente analiza las desventajas de modelado que se enfrentan al usar los lenguajes de entrada de cada verificador de modelos, así como la comparación de los rendimientos de las herramientas al verificar las propiedades de corrección. Se pueden mencionar:

• En 1999, Judi Romijn comparó dos verificadores de modelos ( CADP y SPIN ) en el protocolo de interoperabilidad audio-video HAVi para electrónica de consumo. ^[3]

• En 2003, Yifei Dong, Xiaoqun Du, Gerard J. Holzmann y Scott A. Smolka publicaron una comparación de cuatro verificadores de modelos (a saber: Cospan, Murphi , SPIN y XMC) en un protocolo de comunicación, el protocolo GNU i. ^[4]

• En 2005, Elena M. Bortnik, Nikola Trcka, Anton Wijs, Bas Luttik, JM van de Mortel-Fronczak, Jos CM Baeten, Wan Fokkink y JE Rooda publicaron una comparación de cuatro verificadores de modelos (a saber: CADP , muCRL, SPIN y UPPAAL ) en un sistema de fabricación industrial, una máquina perforadora rotativa. ^[5]

• En 2018, F. Mazzanti y A. Ferrari publicaron una comparación de diez verificadores de modelos (a saber: CADP , CPN Tools, FDR4, NuSMV /nuXmv, mCRL2 , ProB, SPIN , TLA+ , UMC y UPPAAL ) en un problema de supervisión de trenes, teniendo en cuenta tanto la facilidad de uso de los lenguajes como el rendimiento de las herramientas. ^[6]

Competiciones internacionales de software

• Desde 2007, la Competición de Comprobación de Modelos de Hardware (HWMCC) compara el rendimiento de las herramientas de comprobación de modelos orientadas al diseño de hardware.
• Desde 2011, el Concurso de Verificación de Modelos (MCC) compara el rendimiento de las herramientas de verificación de modelos diseñadas para analizar sistemas altamente concurrentes.

Véase también

• AltaRica

Referencias

1. ER Olderog : Semántica de red de Petri operativa para CCSP
2. Rob van Glabbeek, Frits Vaandrager: estructuras de eventos combinados y CCSP
3. Romijn, Judi (junio de 1999). Model Checking a HAVi Leader Election Protocol (informe técnico). Ámsterdam: CWI. SEN-R9915. Archivado desde el original el 2019-09-11 . Consultado el 2018-06-14 .
4. Dong, Yifei; Du, Xiaoqun; Holzmann, Gerard; Smolka, Scott (2003). "Combatiendo el bloqueo en tiempo real en el protocolo i de GNU: un estudio de caso sobre la comprobación de modelos de estado explícito". Herramienta de software para la transferencia de tecnología . 4 (4): 505–528.
5. Bortnik, Elena M.; Trcka, Nikola; Wijs, Anton; Luttik, Bas; van de Mortel-Fronczak, JM; Baeten, Jos CM; Fokkink, Wan; Rooda, JE (2005). "Análisis de un modelo chi de un sistema de plato giratorio utilizando Spin, CADP y Uppaal" (PDF) . Revista de métodos lógicos y algebraicos en programación . 65 (2): 51–104. doi : 10.1016/j.jlap.2005.05.001 . Archivado (PDF) desde el original el 27 de enero de 2021 . Consultado el 25 de mayo de 2018 .
6. Mazzanti, Franco; Ferrari, Alessio (2018). "Diez modelos formales diversos para un sistema de supervisión automática de trenes CBTC". Actas del 3.er taller sobre modelos para el análisis formal de sistemas reales y 6.º taller internacional sobre verificación y transformación de programas (MARS/VPT'18), Tesalónica, Grecia . Actas electrónicas en informática teórica. Vol. 268. págs. 104–149. arXiv : 1803.10324v1 . doi :10.4204/EPTCS.268.4.

Enlaces externos

• Herramientas: una base de datos para herramientas de verificación
• Una lista de herramientas de verificación y síntesis (repositorio de dominio público en GitHub)
• Una lista de herramientas de verificación para sistemas probabilísticos, estocásticos, híbridos y cronometrados

Puntos de referencia comunes

• MCC (modelos del Concurso de Comprobación de Modelos): una colección de cientos de redes de Petri provenientes de numerosos estudios de casos académicos e industriales.
• VLTS (Very Large Transition Systems): una colección de sistemas de transición etiquetados de tamaño creciente, utilizados en muchas publicaciones científicas.