Construcción y análisis de procesos distribuidos

CADP ^{[ 1 ]} ( Construction and Analysis of Distributed Processes ) es una caja de herramientas para el diseño de protocolos de comunicación y sistemas distribuidos. CADP es desarrollado por el equipo CONVECS (anteriormente del equipo VASY) en INRIA Rhone-Alpes y está conectado a diversas herramientas complementarias. CADP se mantiene, se mejora periódicamente y se utiliza en numerosos proyectos industriales.

El objetivo del conjunto de herramientas CADP es facilitar el diseño de sistemas fiables 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 presente concurrencia asíncrona, es decir, cualquier sistema cuyo comportamiento pueda modelarse como un conjunto de procesos paralelos regidos por una semántica de entrelazamiento. Por lo tanto, CADP se puede utilizar para diseñar arquitecturas de hardware, algoritmos distribuidos, protocolos de telecomunicaciones, etc. Las técnicas de verificación enumerativa (también conocidas como verificación explícita de estado) implementadas en CADP, si bien son menos generales que la demostración de teoremas, permiten la detección automática y rentable de errores de diseño en sistemas complejos.

CADP incluye herramientas para apoyar el uso de dos enfoques en métodos formales, ambos 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 los autómatas, las redes de autómatas comunicantes, las redes de Petri, los diagramas de decisión binarios, los sistemas de ecuaciones booleanas, etc. Desde un punto de vista teórico, la investigación sobre modelos busca resultados generales, independientes de cualquier lenguaje de descripción en particular.
• En la práctica, los modelos suelen ser demasiado elementales para describir directamente sistemas complejos (lo que resultarí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.

El desarrollo de CADP comenzó en 1986 con la creación de las dos primeras herramientas: CAESAR y ALDEBARAN. En 1989, se acuñó el acrónimo CADP, que significaba Paquete de Distribución CAESAR/ALDEBARAN . Con el tiempo, se añadieron varias herramientas, incluyendo interfaces de programación que permitieron la contribución de herramientas; el acrónimo CADP pasó a ser Paquete de Desarrollo CAESAR/ALDEBARAN . Actualmente, CADP contiene más de 50 herramientas. Si bien se conserva el mismo acrónimo, el nombre del conjunto de herramientas se ha modificado para reflejar mejor su propósito: Construcción y Análisis de Procesos Distribuidos .

CADP ofrece un amplio conjunto de funcionalidades, que van desde la simulación paso a paso hasta la verificación de modelos masivamente paralela . Incluye:

• Compiladores para varios formalismos de entrada:
  • Descripciones de protocolos 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 a código C para ser utilizado con fines de simulación, verificación y prueba.
  • Descripciones de protocolos de bajo nivel especificadas como máquinas de estados finitos.
  • Redes de autómatas comunicantes, es decir, máquinas de estados finitos que funcionan en paralelo y de forma sincronizada (ya sea mediante operadores de álgebra de procesos o vectores de sincronización).
• Varias herramientas de verificación de equivalencia (minimización y comparaciones módulo relaciones de bisimulación), como BCG_MIN y BISIMULATOR.
• Existen varios verificadores de modelos para diversas lógicas temporales y cálculo mu, como EVALUATOR y XTL.
• Combinación de varios algoritmos de verificación: verificación enumerativa, verificación sobre la marcha, verificación simbólica mediante diagramas de decisión binarios, minimización compositiva, órdenes parciales, comprobación de modelos distribuidos, etc.
• Además, incluye otras herramientas con funcionalidades avanzadas como la verificación visual , la evaluación del rendimiento, etc.

CADP está diseñado de forma modular y hace hincapié en los formatos intermedios y las 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 diversos lenguajes de especificación.

CADP se distribuye gratuitamente a universidades y centros de investigación públicos. Los usuarios de la industria pueden obtener una licencia de evaluación para uso no comercial durante un período limitado, tras el cual se requiere una licencia completa. Para solicitar una copia de CADP, complete el formulario de registro en ^{[ 3 ]} . Una vez firmado el acuerdo de licencia, recibirá instrucciones sobre cómo descargar e instalar CADP.

La caja de herramientas contiene varias herramientas:

• CAESAR.ADT ^{[ 4 ]} es un compilador que traduce los tipos de datos abstractos de LOTOS a tipos y funciones de C. La traducción implica técnicas de compilación basadas en la coincidencia de patrones y el reconocimiento automático de los tipos habituales (enteros, enumeraciones, tuplas, etc.), que se implementan de forma óptima.
• CAESAR ^{[ 5 ]} es un compilador que traduce procesos LOTOS a código C (para prototipado y pruebas rápidas) o a grafos finitos (para verificación). La traducción se realiza mediante varios pasos intermedios, entre los que se incluye la construcción de una red de Petri con variables tipadas, funciones de manejo de datos y transiciones atómicas.
• OPEN/CAESAR ^{[ 6 ]} es un entorno de software genérico para desarrollar herramientas que exploran grafos en tiempo real (por ejemplo, herramientas de simulación, verificación y generación de pruebas). Estas herramientas pueden desarrollarse independientemente de cualquier lenguaje de alto nivel en particular. En este sentido, OPEN/CAESAR desempeña un papel central en el CADP al conectar herramientas orientadas a lenguajes con herramientas orientadas a modelos. OPEN/CAESAR consta de un conjunto de 16 bibliotecas de código 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 gestiona tablas de estados, transiciones, etiquetas, etc.

Se han desarrollado diversas herramientas dentro del entorno OPEN/CAESAR:

• • BISIMULATOR, que comprueba las equivalencias de bisimulación y los pedidos anticipados.
  • CUNCTATOR, que realiza simulaciones de estado estacionario sobre la marcha.
  • DETERMINATOR, que elimina el no determinismo estocástico en sistemas normales, probabilísticos o estocásticos.
  • DISTRIBUTOR, que genera el grafo de estados alcanzables utilizando varias máquinas.
  • EVALUADOR, que evalúa fórmulas regulares de cálculo mu sin alternancia.
  • EJECUTOR, que realiza la ejecución aleatoria de código.
  • EXHIBITOR, que busca secuencias de ejecución que coincidan con una expresión regular dada.
  • GENERADOR, que construye el grafo de estados alcanzables
  • PREDICTOR, que predice la viabilidad del análisis de alcanzabilidad ,
  • PROYECTOR, que calcula abstracciones de sistemas comunicantes.
  • REDUCTOR, que construye y minimiza el grafo de estados alcanzables módulo diversas 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 tanto un formato de archivo para almacenar gráficos muy grandes en disco (utilizando técnicas de compresión eficientes) como un entorno de software para gestionar este formato, incluyendo la partición de gráficos para el procesamiento distribuido. BCG también desempeña un papel fundamental en CADP, ya que muchas herramientas dependen de este formato para sus entradas y salidas. El entorno BCG consta de varias bibliotecas con sus interfaces de programación y de diversas herramientas, entre las que se incluyen:
  • BCG_DRAW, que construye una vista bidimensional de un gráfico,
  • BCG_EDIT permite modificar de forma interactiva el diseño del gráfico producido por Bcg_Draw.
  • BCG_GRAPH, que genera diversas formas de gráficos de utilidad práctica.
  • 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 renombra (mediante expresiones regulares) las etiquetas de transición de un gráfico.
  • BCG_MERGE, que reúne fragmentos de grafos obtenidos de la construcción de grafos distribuidos.
  • BCG_MIN, que minimiza un grafo módulo equivalencias fuertes o de ramificación (y también puede manejar sistemas probabilísticos y estocásticos).
  • BCG_STEADY, que realiza análisis numéricos en estado estacionario de cadenas de Markov de tiempo continuo (extendidas)
  • BCG_TRANSIENT, que realiza análisis numéricos transitorios de cadenas de Markov de tiempo continuo (extendidas)
  • PBG_CP, que copia un grafo BCG particionado
  • PBG_INFO, que muestra información sobre un gráfico BCG particionado
  • PBG_MV mueve un grafo BCG particionado
  • PBG_RM, que elimina un gráfico BCG particionado
  • XTL (eXecutable Temporal Language) es un lenguaje funcional de alto nivel para programar algoritmos de exploración en grafos BCG. XTL proporciona primitivas para manejar estados, transiciones, etiquetas, funciones de sucesor y predecesor, etc. Por ejemplo, se pueden definir funciones recursivas en conjuntos de estados, lo que permite especificar en XTL algoritmos de punto fijo para la generación de diagnósticos y evaluación de lógicas temporales habituales (como HML, ^{[ 7 ]} CTL, ^{[ 8 ]} ACTL, ^{[ 9 ]} etc.).

La conexión entre los modelos explícitos (como los grafos BCG) y los modelos implícitos (explorados sobre la marcha) está garantizada por compiladores compatibles con OPEN/CAESAR, entre los que se 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

El conjunto de herramientas CADP también incluye herramientas adicionales, como ALDEBARAN y TGV (Generación de pruebas basada en la verificación), desarrolladas por el laboratorio Verimag (Grenoble) y el equipo del proyecto Vertecs de INRIA Rennes.

Las herramientas CADP están bien integradas y se puede acceder a ellas fácilmente mediante la interfaz gráfica EUCALYPTUS o el lenguaje de scripting SVL ^{[ 10 ]} . Tanto EUCALYPTUS como SVL proporcionan a los usuarios un acceso sencillo y uniforme a las herramientas CADP, realizando conversiones de formato de archivo automáticamente cuando sea necesario y ofreciendo las opciones de línea de comandos adecuadas al invocar las herramientas.

• En 2002, Radu Mateescu, quien diseñó y desarrolló el verificador de modelos EVALUATOR de CADP, recibió el Premio de Tecnologías 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 para los problemas paralelos del desafío RERS al usar CADP para evaluar con éxito y correctamente 360 ​​fórmulas de lógica de árbol computacional (CTL) y lógica temporal lineal (LTL) en varios conjuntos de máquinas de estados comunicantes. ^{[ 13 ] [ 14 ]}

• En 2020, Frédéric Lang, Franco Mazzanti y Wendelin Serwe ganaron tres medallas de oro en el desafío RERS'2020 al resolver correctamente el 88% de los problemas de "CTL paralelo", dando respuestas de "no sé" solo para 11 fórmulas de 90. ^{[ 15 ] [ 16 ] [ 17 ]}

• En 2021, Hubert Garavel, Frédéric Lang, Radu Mateescu y Wendelin Serwe ganaron conjuntamente el Premio a la Innovación de Inria – Académie des sciences – Dassault Systèmes por su trabajo científico que condujo al desarrollo de la caja de herramientas CADP. ^{[ 18 ]}

• En 2023, Hubert Garavel, Frédéric Lang, Radu Mateescu y Wendelin Serwe recibieron conjuntamente, por la caja de herramientas CADP, el primer premio Test-of-Time Tool Award de ETAPS , el principal foro europeo de ciencia del software. ^{[ 19 ]}

• Generador de compiladores de sintaxis (utilizado para construir muchos compiladores y traductores CADP )

• http://cadp.inria.fr/
• http://vasy.inria.fr/
• http://convecs.inria.fr/