Построение и анализ распределенных процессов
-
Обзор CADP
- CADP — это инструмент для проверки надежности сложных систем, разработанный в INRIA.
- CADP использует формальную семантику для проверки систем с бесконечным числом состояний.
- CADP работает с моделями, представленными в явном виде или неявно, в зависимости от их размера.
-
Языки и методы компиляции
- CADP основан на описании системы LOTOS, которая объединяет концепции алгебр процессов и абстрактных алгебраических типов данных.
- LOTOS позволяет описывать как асинхронные параллельные процессы, так и сложные структуры данных.
- E-LOTOS, обновленная версия LOTOS, обеспечивает большую выразительность и удобство для пользователя.
-
Лицензирование и установка
- CADP распространяется бесплатно среди университетов и государственных исследовательских центров.
- Промышленные пользователи могут получить ознакомительную лицензию.
- Для получения копии CADP необходимо заполнить регистрационную форму и подписать лицензионное соглашение.
-
Краткое описание инструментов
- CADP включает в себя компиляторы для преобразования LOTOS в C и C++, а также инструменты для верификации и анализа.
- Инструменты CADP включают в себя BCG для двумерного представления графиков и XTL для функционального программирования алгоритмов исследования на графах.
-
Награды
- Раду Матееску получил награду за разработку модуля проверки моделей для CADP в 2002 году.
- Хьюберт Гаравель получил премию Гей-Люссака Гумбольдта в 2011 году за вклад в CADP.
- Фредерик Ланг и Франко Маццанти получили золотые медали за решение задач в рамках RERS challenge в 2019 и 2020 годах.
- Юбер Гаравель, Фредерик Ланг, Раду Матееску и Венделин Серве получили премию Inria — Академии наук Dassault Systèmes в 2021 году за разработку CADP.
- Хьюберт Гаравель, Фредерик Ланг, Раду Матееску и Венделин Серве получили награду за инструмент, проверенный временем, от ETAPS в 2023 году.