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 por el equipo VASY) en INRIA Rhone-Alpes y está conectado a varias herramientas complementarias. CADP se mantiene, se mejora regularmente y se utiliza en muchos proyectos industriales.

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.

El CADP se puede aplicar a cualquier sistema que comprenda concurrencia asincrónica, es decir, cualquier sistema cuyo comportamiento se pueda modelar como un conjunto de procesos paralelos regidos por una semántica entrelazada. Por lo tanto, el 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 el 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, ambos necesarios para el diseño de sistemas confiables:

• Los modelos proporcionan representaciones matemáticas para programas paralelos y problemas de verificación relacionados. Algunos ejemplos de modelos son los autómatas, las redes de autómatas que se comunican, 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, independientemente de cualquier lenguaje de descripción particular.
• En la práctica, los modelos suelen ser demasiado elementales para describir sistemas complejos directamente (lo que 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.

El trabajo sobre CADP comenzó en 1986, cuando se emprendió el desarrollo de las dos primeras herramientas, CAESAR y ALDEBARAN. En 1989, se acuñó el acrónimo CADP, que significaba CAESAR/ALDEBARAN Distribution Package . Con el tiempo, se agregaron varias herramientas, incluidas interfaces de programación que permitían contribuir con herramientas: el acrónimo CADP se convirtió entonces en CAESAR/ALDEBARAN Development Package . Actualmente CADP contiene más de 50 herramientas. Si bien se mantiene 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 .

Las versiones de CADP han sido nombradas sucesivamente con letras alfabéticas (de la "A" a la "Z"), luego con los nombres de ciudades que albergan grupos de investigación académica que trabajan activamente en el lenguaje LOTOS y, de forma más general, con los nombres de ciudades en las que se han realizado importantes contribuciones a la teoría de la concurrencia .

Entre los lanzamientos principales, suelen estar disponibles lanzamientos menores que brindan acceso anticipado a nuevas funciones y mejoras. Para obtener más información, consulte la página de lista de cambios en el sitio web de CADP.

CADP ofrece un amplio conjunto de funcionalidades, que van desde la simulación paso a paso hasta la verificación masiva de modelos en paralelo . 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 usarse 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 funcionan en paralelo y sincronizadas (ya sea utilizando operadores de álgebra de procesos o vectores de sincronización).
• Varias herramientas de comprobación de equivalencia (minimización y comparaciones módulo relaciones de bisimulación), como BCG_MIN y BISIMULATOR.
• Varios verificadores de modelos para diversas lógicas temporales y cálculos 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 compositiva, órdenes parciales, verificación de modelos distribuidos, etc.
• Además de otras herramientas con funcionalidades avanzadas como verificación visual, evaluación de rendimiento, etc.

CADP está diseñado de forma modular y pone énfasis 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 diversos lenguajes de especificació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 grafos), que consiste en un conjunto de estados, un estado inicial y una relación de transición entre estados. Este modelo se genera a menudo de forma automática a partir de descripciones de alto nivel del sistema en estudio, y luego se compara con las propiedades del sistema mediante diversos procedimientos de decisión. Según el formalismo utilizado para expresar las propiedades, existen dos enfoques posibles:

• 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 para la verificación es la comprobació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 comprobación de equivalencia que comparan y minimizan los autómatas módulo varias relaciones de equivalencia y 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 comprobació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 de lógica temporal. En tal caso, el enfoque natural para la verificación es la comprobación del modelo , que consiste en decidir si el modelo del sistema satisface o no las propiedades lógicas. CADP contiene herramientas de comprobación de modelos para una forma poderosa de lógica temporal, el cálculo mu modal, que se extiende con variables tipificadas y expresiones 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 estados, que se produce cuando los modelos son demasiado grandes para caber en la memoria del ordenador. CADP proporciona tecnologías de software para manejar modelos de dos formas complementarias:

• Los modelos pequeños se pueden representar explícitamente, almacenando en memoria todos sus estados y transiciones (verificación exhaustiva);
• Los modelos más grandes se representan implícitamente, explorando solo los estados y las transiciones del modelo necesarios para la verificación (verificación sobre la marcha).

La especificación precisa de sistemas complejos y fiables requiere un lenguaje que sea ejecutable (para verificación enumerativa) y que tenga semántica formal (para evitar ambigüedades del lenguaje que podrían llevar a divergencias de interpretación entre diseñadores e implementadores). La semántica formal también es necesaria cuando es necesario establecer la corrección de un sistema infinito; esto no se puede hacer utilizando técnicas enumerativas porque tratan solo con abstracciones finitas, por lo que se debe hacer utilizando técnicas de demostración de teoremas, que solo se aplican a lenguajes con 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 (norma ISO/IEC 8807:1989), que combina los conceptos de álgebras de procesos (en particular CCS y CSP) y tipos de datos abstractos algebraicos. De este modo, LOTOS puede describir tanto procesos concurrentes asincrónicos como estructuras de datos complejas.

LOTOS fue revisado en profundidad en 2001, lo que dio lugar a la publicación de E-LOTOS (Enhanced-Lotos, estándar ISO/IEC 15437:2001), que intenta proporcionar una mayor expresividad (por ejemplo, introduciendo tiempo cuantitativo para describir sistemas con restricciones de tiempo real) junto con una mejor facilidad de uso.

Existen varias herramientas para convertir descripciones en otros cálculos de procesos o formatos intermedios a LOTOS, de modo que luego se puedan utilizar las herramientas CADP para la verificación.

CADP se distribuye de forma gratuita 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] Una vez que se haya firmado el acuerdo de licencia, recibirá detalles 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 en tipos y funciones de 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 forma óptima.
• CAESAR ^[5] es un compilador que traduce los procesos LOTOS a código C (para fines de creación rápida de prototipos y pruebas) o a grafos 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, funciones 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 lenguaje de alto nivel en particular. En este sentido, OPEN/CAESAR desempeña un papel central en CADP al conectar herramientas orientadas al lenguaje con herramientas orientadas al modelo. OPEN/CAESAR consta de un conjunto de 16 bibliotecas de código con sus interfaces de programación, 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 comprueba equivalencias de bisimulación y preordenes
  • CUNCTATOR, que realiza simulaciones 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
  • EVALUADOR, que evalúa fórmulas regulares de cálculo mu libres de alternancia
  • EJECUTOR, que realiza la ejecución aleatoria de código
  • EXPOSITOR, que busca secuencias de ejecución que coincidan con una expresión regular dada
  • GENERADOR, que construye el gráfico de estados alcanzables
  • PREDICTOR, que predice la viabilidad del análisis de alcanzabilidad,
  • PROYECTOR, que calcula abstracciones de sistemas de comunicación
  • REDUCTOR, que construye y minimiza el gráfico 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 bloqueo
• 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, incluida la partición de gráficos para el procesamiento distribuido. BCG también desempeña 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, entre las que se incluyen:
  • BCG_DRAW, que crea una vista bidimensional de un gráfico,
  • BCG_EDIT que permite modificar de forma interactiva el diseño del 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 renombra (usando expresiones regulares) las etiquetas de transición de un gráfico
  • BCG_MERGE, que reúne fragmentos de gráficos obtenidos a partir de la construcción de gráficos distribuidos
  • BCG_MIN, que minimiza un gráfico módulo equivalencias fuertes o ramificadas (y también puede tratar con sistemas probabilísticos y estocásticos)
  • BCG_STEADY, que realiza análisis numérico de estado estable de cadenas de Markov de tiempo continuo (extendidas)
  • BCG_TRANSIENT, que realiza 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 la programación de algoritmos de exploración en grafos BCG. XTL proporciona primitivas para manejar estados, transiciones, etiquetas, funciones sucesoras y predecesoras, etc. Por ejemplo, se pueden definir funciones recursivas sobre conjuntos de estados, que permiten especificar en XTL algoritmos de punto fijo de evaluación y generación de diagnósticos para lógicas temporales usuales (como HML, ^[7] CTL, ^[8] ACTL, ^[9] etc.).

La conexión entre modelos explícitos (como gráficos BCG) y modelos implícitos (explorados sobre la marcha) está garantizada por compiladores compatibles con OPEN/CAESAR, incluidos:

• • CESAR.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 rastros de ejecución

La caja de herramientas CADP también incluye herramientas adicionales, como ALDEBARAN y TGV (Generación de pruebas basada en verificación) desarrolladas por el laboratorio Verimag (Grenoble) y el equipo del proyecto Vertecs del 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 programación SVL ^[10] . Tanto EUCALYPTUS como SVL proporcionan a los usuarios un acceso fácil y uniforme a las herramientas CADP realizando conversiones de formato de archivo automáticamente cuando sea necesario y proporcionando opciones de línea de comandos adecuadas a medida que se invocan las herramientas.

• 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 10ª 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 en 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 "CTL paralelos", dando solo respuestas de "no sé" 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 SYNTAX (utilizado para crear muchos compiladores y traductores CADP )

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