CADP [1] (Construcción y Análisis de Procesos Distribuidos) es una caja de herramientas para el diseño de protocolos de comunicación y sistemas distribuidos. CADP es desarrollado por el equipo de CONVECS (anteriormente por el equipo de VASY) en INRIA Rhone-Alpes y conectado a varias herramientas complementarias. El CADP se mantiene, se mejora periódicamente y se utiliza en muchos proyectos industriales.
![]() | |
Desarrollador (es) | Equipo INRIA CONVECS (anteriormente equipo VASY ) |
---|---|
Versión inicial | 1989, hace 31–32 años |
Lanzamiento estable | 2020/13 de diciembre de 2020 |
Sistema operativo | Windows , macOS , Linux , Solaris y OpenIndiana |
Tipo | Caja de herramientas para diseñar protocolos de comunicación y sistemas distribuidos |
Sitio web | cadp |
El propósito del kit de herramientas CADP es facilitar el diseño de sistemas confiables mediante el uso de técnicas de descripción formal junto con herramientas de software para simulación, desarrollo rápido de aplicaciones , verificación y generación de pruebas.
CADP se puede aplicar a cualquier sistema que comprenda concurrencia asincrónica, es decir, cualquier sistema cuyo comportamiento pueda modelarse como un conjunto de procesos paralelos gobernados por semántica entrelazada. Por lo tanto, CADP se puede utilizar para diseñar arquitectura de hardware, algoritmos distribuidos, protocolos de telecomunicaciones, etc. Las técnicas de verificación enumerativa (también conocida como verificación explícita de estado) implementadas en CADP, aunque menos generales que la demostración de teoremas, permiten una detección automática y rentable. de errores de diseño en sistemas complejos.
CADP incluye herramientas para respaldar el uso de dos enfoques en métodos formales, los cuales son necesarios para el diseño de sistemas confiables:
- Los modelos proporcionan representaciones matemáticas para programas paralelos y problemas de verificación relacionados. Ejemplos de modelos son autómatas, redes de autómatas comunicantes, redes de Petri, diagramas de decisión binarios, sistemas de ecuaciones booleanas, etc. Desde un punto de vista teórico, la investigación de modelos busca resultados generales, independientes de cualquier lenguaje descriptivo particular.
- En la práctica, los modelos suelen ser demasiado elementales para describir sistemas complejos directamente (esto sería tedioso y propenso a errores). Para esta tarea se necesita un formalismo de nivel superior conocido como álgebra de procesos o cálculo de procesos , así como compiladores que traduzcan descripciones de alto nivel en modelos adecuados para algoritmos de verificación.
Historia
El CADP comenzó a trabajar en 1986, cuando se emprendió el desarrollo de las dos primeras herramientas, CAESAR y ALDEBARAN. En 1989 se acuñó el acrónimo CADP, que significa Paquete de Distribución CAESAR / ALDEBARAN . Con el tiempo, se agregaron varias herramientas, incluyendo interfaces de programación que permitieron aportar herramientas: el acrónimo CADP pasó a ser el Paquete de Desarrollo CAESAR / ALDEBARAN . Actualmente CADP contiene más de 50 herramientas. Manteniendo el mismo acrónimo, se ha cambiado el nombre de la caja de herramientas para indicar mejor su propósito: Construcción y Análisis de Procesos Distribuidos .
Lanzamientos importantes
Los lanzamientos de CADP se han nombrado sucesivamente con letras alfabéticas (de la "A" a la "Z"), luego con los nombres de las ciudades que albergan grupos de investigación académica que trabajan activamente en el lenguaje LOTOS y, de manera más general, los nombres de las ciudades en las que Se han hecho contribuciones a la teoría de la concurrencia .
Nombre clave | Fecha |
---|---|
"A" ... "Z" | Enero de 1990 - diciembre de 1996 |
Twente | Junio de 1997 |
Feudal | Enero de 1999 |
Ottawa | Julio de 2001 |
Edimburgo | Diciembre de 2006 |
Zúrich | diciembre 2013 |
Amsterdam | Diciembre de 2014 |
Stony Brook | Diciembre de 2015 |
Oxford | Diciembre de 2016 |
Sophia Antipolis | Diciembre de 2017 |
Upsala | Diciembre de 2018 |
Pisa | Diciembre de 2019 |
Aalborg | Diciembre de 2020 |
Entre las versiones principales, las versiones secundarias a menudo están disponibles, lo que brinda acceso temprano a nuevas funciones y mejoras. Para obtener más información, consulte la página de la lista de cambios en el sitio web de CADP.
Funciones CADP
CADP ofrece un amplio conjunto de funcionalidades, que van desde la simulación paso a paso hasta la verificación masiva de modelos paralelos . Incluye:
- Compiladores para varios formalismos de entrada:
- Descripciones de protocolo de alto nivel escritas en el lenguaje ISO LOTOS . [2] La caja de herramientas contiene dos compiladores (CAESAR y CAESAR.ADT) que traducen las descripciones de LOTOS en código C para su uso con fines de simulación, verificación y prueba.
- Descripciones de protocolo de bajo nivel especificadas como máquinas de estados finitos.
- Redes de autómatas comunicantes, es decir, máquinas de estados finitos que se ejecutan en paralelo y sincronizadas (ya sea utilizando operadores de álgebra de procesos o vectores de sincronización).
- Varias herramientas de comprobación de equivalencias (minimización y comparaciones modulo de relaciones de bisimulación), como BCG_MIN y BISIMULATOR.
- Varios verificadores de modelos para varios cálculos de lógica temporal y mu, como EVALUATOR y XTL.
- Varios algoritmos de verificación combinados: verificación enumerativa, verificación sobre la marcha, verificación simbólica mediante diagramas de decisión binarios, minimización de composición, órdenes parciales, verificación de modelos distribuidos, etc.
- Además de otras herramientas con funcionalidades avanzadas como verificación visual , evaluación de desempeño, etc.
CADP está diseñado de forma modular y hace hincapié en formatos intermedios e interfaces de programación (como los entornos de software BCG y OPEN / CAESAR), que permiten combinar las herramientas CADP con otras herramientas y adaptarlas a varios lenguajes de especificación.
Modelos y técnicas de verificación
La verificación es la comparación de un sistema complejo con un conjunto de propiedades que caracterizan el funcionamiento previsto del sistema (por ejemplo, libertad de bloqueo, exclusión mutua, equidad, etc.).
La mayoría de los algoritmos de verificación en CADP se basan en el modelo de sistemas de transición etiquetados (o, simplemente, autómatas o gráficos), que consta de un conjunto de estados, un estado inicial y una relación de transición entre estados. Este modelo a menudo se genera automáticamente a partir de descripciones de alto nivel del sistema en estudio, luego se compara con las propiedades del sistema utilizando varios procedimientos de decisión. Dependiendo del formalismo utilizado para expresar las propiedades, son posibles dos enfoques:
- Las propiedades de comportamiento expresan el funcionamiento previsto del sistema en forma de autómatas (o descripciones de nivel superior, que luego se traducen en autómatas). En tal caso, el enfoque natural de la verificación es la verificación de equivalencia , que consiste en comparar el modelo del sistema y sus propiedades (ambos representados como autómatas) módulo alguna equivalencia o relación de preorden. CADP contiene herramientas de verificación de equivalencia que comparan y minimizan el módulo de autómatas de varias equivalencias y relaciones de preorden; Algunas de estas herramientas también se aplican a modelos estocásticos y probabilísticos (como las cadenas de Markov). CADP también contiene herramientas de verificación visual que se pueden utilizar para verificar una representación gráfica del sistema.
- Las propiedades lógicas expresan el funcionamiento previsto del sistema en forma de fórmulas lógicas temporales. En tal caso, el enfoque natural de la verificación es la verificación del modelo , que consiste en decidir si el modelo del sistema satisface o no las propiedades lógicas. CADP contiene herramientas de verificación de modelos para una forma poderosa de lógica temporal, el cálculo mu modal, que se amplía con variables y expresiones escritas para expresar predicados sobre los datos contenidos en el modelo. Esta extensión proporciona propiedades que no podrían expresarse en el cálculo mu estándar (por ejemplo, el hecho de que el valor de una variable dada siempre aumenta a lo largo de cualquier ruta de ejecución).
Aunque estas técnicas son eficientes y automatizadas, su principal limitación es el problema de explosión de estado, que ocurre cuando los modelos son demasiado grandes para caber en la memoria de la computadora. CADP proporciona tecnologías de software para manejar modelos de dos formas complementarias:
- Los modelos pequeños se pueden representar de forma explícita, almacenando en la memoria todos sus estados y transiciones (verificación exhaustiva);
- Los modelos más grandes se representan implícitamente, explorando solo los estados del modelo y las transiciones necesarias para la verificación (verificación sobre la marcha).
Idiomas y técnicas de compilación
La especificación precisa de sistemas complejos y confiables requiere un lenguaje que sea ejecutable (para la verificación enumerativa) y que tenga semántica formal (para evitar ambigüedades del lenguaje que podrían conducir a divergencias de interpretación entre diseñadores e implementadores). La semántica formal también es necesaria cuando es necesaria para establecer la corrección de un sistema infinito; esto no se puede hacer usando técnicas enumerativas porque tratan solo con abstracciones finitas, por lo que debe hacerse usando técnicas de demostración de teoremas, que solo se aplican a lenguajes con una semántica formal.
CADP actúa sobre una descripción LOTOS del sistema. LOTOS es un estándar internacional para la descripción de protocolos (estándar ISO / IEC 8807: 1989), que combina los conceptos de álgebras de procesos (en particular, CCS y CSP y tipos de datos abstractos algebraicos. Por lo tanto, LOTOS puede describir tanto procesos concurrentes asincrónicos como estructuras de datos complejas .
LOTOS fue revisado en gran medida en 2001, lo que dio lugar a la publicación de E-LOTOS (Enhanced-Lotos, norma ISO / IEC 15437: 2001), que intenta proporcionar una mayor expresividad (por ejemplo, mediante la introducción de tiempo cuantitativo para describir sistemas con real- limitaciones de tiempo) junto con una mayor facilidad de uso.
Existen varias herramientas para convertir descripciones en otros cálculos de proceso o formato intermedio en LOTOS, de modo que las herramientas CADP se puedan utilizar para la verificación.
Licencia e instalación
CADP se distribuye gratuitamente a universidades y centros públicos de investigación. Los usuarios de la industria pueden obtener una licencia de evaluación para uso no comercial durante un período de tiempo limitado, después del cual se requiere una licencia completa. Para solicitar una copia de CADP, complete el formulario de registro en. [3] Después de que se haya firmado el acuerdo de licencia, recibirá detalles sobre cómo descargar e instalar CADP.
Resumen de herramientas
La caja de herramientas contiene varias herramientas:
- CAESAR.ADT [4] es un compilador que traduce los tipos de datos abstractos de LOTOS en tipos C y funciones C. La traducción implica técnicas de compilación de coincidencia de patrones y reconocimiento automático de tipos habituales (enteros, enumeraciones, tuplas, etc.), que se implementan de manera óptima.
- CAESAR [5] es un compilador que traduce los procesos de LOTOS en código C (para la creación rápida de prototipos y pruebas) o gráficos finitos (para verificación). La traducción se realiza mediante varios pasos intermedios, entre los que se encuentran la construcción de una red de Petri extendida con variables tipificadas, características de manejo de datos y transiciones atómicas.
- OPEN / CAESAR [6] es un entorno de software genérico para desarrollar herramientas que exploran gráficos sobre la marcha (por ejemplo, herramientas de simulación, verificación y generación de pruebas). Estas herramientas se pueden desarrollar independientemente de cualquier idioma de alto nivel en particular. En este sentido, OPEN / CAESAR juega un papel central en CADP al conectar herramientas orientadas al lenguaje con herramientas orientadas a modelos. OPEN / CAESAR consta de un conjunto de 16 bibliotecas de códigos con sus interfaces de programación, tales como:
- Caesar_Hash, que contiene varias funciones hash
- Caesar_Solve, que resuelve sistemas de ecuaciones booleanas sobre la marcha
- Caesar_Stack, que implementa pilas para la exploración de búsqueda en profundidad
- Caesar_Table, que maneja tablas de estados, transiciones, etiquetas, etc.
Se han desarrollado varias herramientas dentro del entorno OPEN / CAESAR:
- BISIMULATOR, que verifica las equivalencias y preordenes de bisimulación
- CUNCTATOR, que realiza una simulación de estado estable sobre la marcha
- DETERMINADOR, que elimina el no determinismo estocástico en sistemas normales, probabilísticos o estocásticos
- DISTRIBUIDOR, que genera el gráfico de estados alcanzables utilizando varias máquinas
- EVALUATOR, que evalúa fórmulas de cálculo mu regulares sin alternancia
- EXECUTOR, que realiza la ejecución aleatoria de código
- EXPOSITOR, que busca secuencias de ejecución que coincidan con una expresión regular determinada
- GENERATOR, que construye el gráfico de estados alcanzables
- PREDICTOR, que predice la viabilidad del análisis de accesibilidad,
- PROYECTOR, que calcula abstracciones de sistemas de comunicación
- REDUCTOR, que construye y minimiza la gráfica de estados alcanzables módulo varias relaciones de equivalencia
- SIMULATOR, X-SIMULATOR y OCIS, que permiten la simulación interactiva
- TERMINATOR, que busca estados de interbloqueo
- BCG (Binary Coded Graphs) es un formato de archivo para almacenar gráficos muy grandes en el disco (utilizando técnicas de compresión eficientes) y un entorno de software para manejar este formato, incluidos los gráficos de particiones para el procesamiento distribuido. BCG también juega un papel clave en CADP ya que muchas herramientas dependen de este formato para sus entradas / salidas. El entorno BCG consta de varias bibliotecas con sus interfaces de programación y de varias herramientas, que incluyen:
- BCG_DRAW, que crea una vista bidimensional de un gráfico,
- BCG_EDIT que permite modificar interactivamente el diseño gráfico producido por Bcg_Draw
- BCG_GRAPH, que genera varias formas de gráficos prácticamente útiles
- BCG_INFO, que muestra diversa información estadística sobre un gráfico
- BCG_IO, que realiza conversiones entre BCG y muchos otros formatos de gráficos
- BCG_LABELS, que oculta y / o cambia el nombre (usando expresiones regulares) las etiquetas de transición de un gráfico
- BCG_MERGE, que recopila fragmentos de gráficos obtenidos de la construcción de gráficos distribuidos
- BCG_MIN, que minimiza un gráfico módulo fuerte o equivalencias ramificadas (y también puede tratar con sistemas estocásticos y probabilísticos)
- BCG_STEADY, que realiza un análisis numérico de estado estable de cadenas de Markov de tiempo continuo (extendidas)
- BCG_TRANSIENT, que realiza un análisis numérico transitorio de cadenas de Markov de tiempo continuo (extendidas)
- PBG_CP, que copia un gráfico BCG particionado
- PBG_INFO, que muestra información sobre un gráfico BCG particionado
- PBG_MV que mueve un gráfico BCG particionado
- PBG_RM, que elimina un gráfico BCG particionado
- XTL (eXecutable Temporal Language), que es un lenguaje funcional de alto nivel para programar algoritmos de exploración en gráficos BCG. XTL proporciona primitivas para manejar estados, transiciones, etiquetas, funciones sucesoras y predecesoras, etc. Por ejemplo, se pueden definir funciones recursivas en conjuntos de estados, que permiten especificar en la evaluación XTL y la generación de diagnóstico algoritmos de punto fijo para lógicas temporales habituales (tales como HML, [7] CTL, [8] ACTL, [9] etc.).
La conexión entre los modelos explícitos (como los gráficos BCG) y los modelos implícitos (explorados sobre la marcha) está garantizada por compiladores compatibles con OPEN / CAESAR, que incluyen:
- CAESAR.OPEN, para modelos expresados como descripciones LOTOS
- BCG.OPEN, para modelos representados como gráficos BCG
- EXP.OPEN, para modelos expresados como autómatas comunicantes
- FSP.OPEN, para modelos expresados como descripciones FSP
- LNT.OPEN, para modelos expresados como descripciones LNT
- SEQ.OPEN, para modelos representados como conjuntos de trazas de ejecución
La caja de herramientas CADP también incluye herramientas adicionales, como ALDEBARAN y TGV (Test Generation based on Verification) desarrollado por el laboratorio Verimag (Grenoble) y el equipo de proyecto Vertecs de INRIA Rennes.
Las herramientas CADP están bien integradas y se puede acceder a ellas fácilmente utilizando la interfaz gráfica EUCALYPTUS o el lenguaje de programación SVL [10] . Tanto EUCALYPTUS como SVL brindan a los usuarios un acceso fácil y uniforme a las herramientas CADP al realizar conversiones de formato de archivo automáticamente cuando sea necesario y al proporcionar las opciones de línea de comandos adecuadas a medida que se invocan las herramientas.
Premios
- En 2002, Radu Mateescu, que diseñó y desarrolló el verificador de modelos EVALUATOR de CADP, recibió el Premio de Tecnología de la Información otorgado durante la décima edición del simposio anual organizado por la Fundación Rhône-Alpes Futur. [11]
- En 2011, Hubert Garavel, arquitecto de software y desarrollador de CADP, recibió el Premio Gay-Lussac Humboldt . [12]
- En 2019, Frédéric Lang y Franco Mazzanti ganaron todas las medallas de oro por los problemas paralelos del desafío RERS al usar CADP para evaluar con éxito y correctamente las fórmulas de lógica de árbol computacional 360 (CTL) y lógica temporal lineal (LTL) en varios conjuntos de estados de comunicación. máquinas. [13] [14]
Ver también
Referencias
- ^ Garavel H, Lang F, Mateescu R, Serwe W: CADP 2011: una caja de herramientas para la construcción y análisis de procesos distribuidos Revista internacional sobre herramientas de software para la transferencia de tecnología (STTT), 15 (2): 89-107, abril de 2013
- ^ ISO 8807, Lenguaje de especificación de orden temporal
- ^ Formulario de solicitud en línea de CADP . Cadp.inria.fr (30 de agosto de 2011). Consultado el 16 de junio de 2014.
- ^ H. Garavel. Compilación de tipos de datos abstractos de LOTOS , en actas de la 2da Conferencia Internacional sobre Técnicas de Descripción Formal FORTE'89 (Vancouver BC, Canadá), ST Vuong (editor), Holanda Septentrional, diciembre de 1989, p. 147-162.
- ^ H. Garavel, J. Sifakis. Compilación y verificación de las especificaciones de LOTOS , en las actas del décimo simposio internacional sobre especificación, prueba y verificación de protocolos (Ottawa, Canadá), L. Logrippo, RL Probert, H. Ural (editores), Holanda del Norte, IFIP, junio de 1990, pag. 379–394.
- ^ H. Garavel. OPEN / CÆSAR: Una arquitectura de software abierta para verificación, simulación y pruebas , en las actas de la Primera Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y Análisis de Sistemas TACAS'98 (Lisboa, Portugal), Berlín, B. Steffen (editor ), Lecture Notes in Computer Science, versión completa disponible como Inria Research Report RR-3352 , Springer Verlag, marzo de 1998, vol. 1384, pág. 68–84.
- ^ M. Hennessy, R. Milner. Leyes algebraicas para el no determinismo y la concurrencia , en: Journal of the ACM , 1985, vol. 32, pág. 137-161.
- ^ EM Clarke, EA Emerson, AP Sistla. Verificación automática de sistemas concurrentes de estados finitos usando especificaciones lógicas temporales , en: Transacciones ACM sobre lenguajes y sistemas de programación , abril de 1986, vol. 8, no 2, pág. 244–263.
- ^ R. De Nicola, FW Vaandrager. Acción versus lógica basada en el estado para sistemas de transición , Lecture Notes in Computer Science , Springer Verlag, 1990, vol. 469, pág. 407–419.
- ^ H. Garavel, F. Lang. SVL: a Scripting Language for Compositional Verification , en: Actas de la 21a Conferencia Internacional IFIP WG 6.1 sobre Técnicas Formales para Sistemas en Red y Distribuidos FORTE'2001 (Isla Cheju, Corea), M. Kim, B. Chin, S. Kang, D. Lee (editores), versión completa disponible como Inria Research Report RR-4223 , Kluwer Academic Publishers, IFIP, agosto de 2001, p. 377–392.
- ^ "Radu Mateescu gana el premio de TI otorgado por Fondation Rhône-Alpes Futur" .
- ^ Isabelle Bellin (16 de abril de 2011). "Hubert Garavel recibió el Premio de Investigación Gay-Lussac Humboldt" .
- ^ "Resultados del RERS Challenge 2019" .
- ^ "The CADP Newsletter Nr. 12 - April 10, 2019" .
- ^ "Resultados del RERS Challenge 2020" .
- ^ "Equipo CNR-Inria gana medallas de oro en el RERS 2020 Parallel CTL Challenge" .
- ^ "The CADP Newsletter Nr. 13 - 22 de febrero de 2021" .
enlaces externos
- http://cadp.inria.fr/
- http://vasy.inria.fr/
- http://convecs.inria.fr/