Construction and Analysis of Distributed Processes

CADP применим к любым системам с асинхронным параллелизмом, то есть к системам, которые могут моделироваться как множество параллельных процессов с семантикой перемежения. Поэтому CADP может использоваться для проектирования аппаратных архитектур, распределённых алгоритмов, телекоммуникационных протоколов и других подобных систем. Перечислительная (явная) модель верификации, реализованная в CADP, менее общая, чем автоматическое доказательство теорем, но обеспечивает быстрый и автоматизированный поиск ошибок проектирования в сложных системах.

В состав CADP входят инструменты, поддерживающие два подхода, необходимых для проектирования надёжных систем:

• Модели — это математические представления параллельных программ и связанных задач верификации: автоматы, сети коммуницирующих автоматов, сети Петри, бинарные решающие диаграммы, булевы уравнения и др. В теории исследования моделей стремятся получить общие результаты, независимые от конкретных языков.
• На практике модели слишком элементарны для описания сложных систем напрямую, это было бы трудно и подвержено ошибкам. Для этого используют формализмы высокого уровня, такие как алгебра процессов, а также компиляторы, переводящие эти описания в пригодные для верификации модели.

Работы над CADP начались в 1986 году с разработки первых двух инструментов — CAESAR и ALDEBARAN. В 1989 году был введён акроним CADP, означавший «CAESAR/ALDEBARAN Distribution Package». Позже были добавлены новые инструменты и программные интерфейсы, что позволило интегрировать сторонние компоненты; название стало трактоваться как «CAESAR/ALDEBARAN Development Package». Сейчас CADP включает более 50 инструментов. Несмотря на сохранение акронима, полное название было изменено в соответствии с назначением: «Construction and Analysis of Distributed Processes».

Выпуски CADP получали имена сначала по буквам латинского алфавита («A»—"Z"), затем — именами городов, где работают академические группы, внёсшие крупный вклад в развитие языка LOTOS и теории параллелизма.

Между крупными релизами часто выходят промежуточные минорные версии, дающие ранний доступ к новым возможностям и исправлениям. Подробнее — на странице изменений официального сайта.

CADP предоставляет широкий спектр функций: пошаговое моделирование, высокопроизводительная модельная проверка и др. Среди поддерживаемых возможностей:

• Компиляторы для различных формализмов:
  • Описания протоколов высокого уровня на стандарте LOTOS^[1]. В комплект входят два компилятора (CAESAR и CAESAR.ADT), переводящих LOTOS-описания в C-код для моделирования, тестирования и верификации.
  • Описания протоколов низкого уровня в виде конечных автоматов.
  • Сети коммуницирующих автоматов — конечные автоматы, работающие параллельно (синхронизация операторами алгебры процессов или через векторы синхронизации).
• Инструменты проверки эквивалентности (минимизация, сравнение по бимуляции и др.) — BCG_MIN, BISIMULATOR.
• Модель-чекеры для различных логик времени и μ-исчисления: EVALUATOR, XTL.
• Различные алгоритмы верификации: перечислительная, по ходу построения (on-the-fly), символическая (по решающим диаграммам), композиционная минимизация, частичные порядки, распределённая модельная проверка и другие подходы.
• Дополнительные инструменты: визуальная проверка, оценка производительности и др.

CADP построен по модульному принципу, акцентировано использование промежуточных форматов и открытых интерфейсов (например, среды BCG и OPEN/CAESAR), что позволяет интегрировать инструменты CADP с другими программами и адаптировать под разные языки спецификаций.

Верификация — сравнение сложной системы с набором свойств, определяющих её требуемое поведение (например, отсутствие тупиков, взаимное исключение, справедливость).

Большинство алгоритмов CADP строится на модели помеченных конечных автоматов (labelled transition systems) — граф состояния с начальным состоянием и переходами. Обычно такие модели автоматически строятся по высокоуровневым описаниям, после чего сравниваются с заданными свойствами разными алгоритмами. По способу выражения свойств различают два подхода:

• Поведенческие свойства задаются в виде автоматов (или описаний, переводимых в автоматы). В таком случае применяют проверку эквивалентности: сравнивают модель системы и свойство (оба в виде автоматов) с учётом заданных эквивалентностей или отношений предшествования. Некоторые средства CADP позволяют проверять также вероятностные (например, марковские) и стохастические модели, выполнять визуальную проверку.
• Логические свойства задаются формулами логики времени. Их проверяют методом модельной проверки, определяя, выполняется ли формула на данной модели. Пример — поддержка расширенного модального μ-исчисления с типизированными переменными, что позволяет выразить свойства, невозможные в стандартной логике (например, возрастающую вдоль траектории величину переменной).

Эти методы автоматизированы и эффективны, но ограничены проблемой взрыва состояний (state explosion), когда модель слишком велика для размещения в памяти. Для борьбы с этим CADP поддерживает два подхода:

• Малые модели размещаются полностью в памяти (полная переборная верификация);
• Крупные модели проверяются путём динамического построения только нужных частей (on-the-fly verification).

Для спецификации надёжных сложных систем требуется язык, пригодный для исполнения (переборных методов) и с формальной семантикой (чтобы избежать неоднозначности и поддерживать доказательства корректности для бесконечных систем).

CADP работает с описаниями системы на языке LOTOS, международном стандарте для протоколов (ISO/IEC 8807:1989), который совмещает подход алгебр процессов (CCS, CSP) и абстрактных типов данных. LOTOS допускает описание как асинхронных параллельных процессов, так и сложных структур данных.

В 2001 году LOTOS существенно переработан: появился стандарт E-LOTOS (ISO/IEC 15437:2001), обладающий большей выразительностью (например, введено описание времени/реального времени) и улучшенной удобством пользователя.

Существуют инструменты для преобразования описаний из других исчислений процессов или промежуточных форматов в LOTOS, что делает возможным применение инструментов CADP для анализа таких моделей.

Поддерживаются основные операционные системы: Windows, macOS, Linux, Solaris, OpenIndiana.

CADP распространяется бесплатно для университетов и научных учреждений. Промышленные пользователи могут получить оценочную лицензию для некоммерческого использования на ограниченное время, по окончании которого требуется полная лицензия. Для получения копии необходимо заполнить регистрационную форму на сайте^[2]. После подписания лицензионного соглашения вы получите инструкции по скачиванию и установке.

В состав CADP входят многочисленные инструменты, среди которых:

• CAESAR.ADT^[3] — компилятор, переводящий абстрактные типы данных LOTOS в типы и функции на языке C (реализует техники сопоставления с образцом и автоматическое определение стандартных типов).
• CAESAR^[4] — компилятор LOTOS-процессов в код на языке C (для быстрого прототипирования и тестирования) или в конечные графы (для верификации); строит, в частности, сеть Петри с типизированными переменными.
• OPEN/CAESAR^[5] — программная среда для разработки инструментов исследования графов по ходу построения (симуляция, тестирование, верификация и др.), не зависящих от конкретного языка описания; состоит из 16 библиотек и интерфейсов, включая:
  • Caesar_Hash (хэш-функции), Caesar_Solve (решение булевых уравнений), Caesar_Stack (реализация стека для обхода в глубину), Caesar_Table (таблицы состояний, переходов и меток).

На базе OPEN/CAESAR построен ряд инструментов:

• • BISIMULATOR (проверка бимуляций), CUNCTATOR (имитация стационарного состояния), DETERMINATOR (устранение стохастического недетерминизма), DISTRIBUTOR (распределённое построение графа достижимости), EVALUATOR (проверка формул μ-исчисления без перемежений), EXECUTOR (случайное исполнение кода), EXHIBITOR (поиск последовательностей по регулярному выражению), GENERATOR (построение графа достижимости), PREDICTOR (прогноз выполнимости анализа достижимости), PROJECTOR (вычисление абстрактных моделей), REDUCTOR (минимизация графа достижимости), SIMULATOR / X-SIMULATOR / OCIS (интерактивное моделирование), TERMINATOR (поиск тупиковых состояний).
• BCG (Binary Coded Graphs) — формат файлов для хранения больших графов с сжатием и программная среда для их обработки (поддержка распределённой работы). Окружение BCG включает библиотеки и набор инструментов:
  • BCG_DRAW (двумерное визуальное представление графа), BCG_EDIT (интерактивное редактирование), BCG_GRAPH (генерация полезных графов), BCG_INFO (статистическая информация), BCG_IO (конвертация между форматами), BCG_LABELS (скрытие и переименование меток переходов), BCG_MERGE (слияние фрагментов графа), BCG_MIN (минимизация по сильной/ветвящейся эквивалентности, поддержка вероятностных и стохастических моделей), BCG_STEADY и BCG_TRANSIENT (статистическая и переходная анализа марковских моделей), PBG_CP / INFO / MV / RM (работа с партиционированными графами).
  • XTL (eXecutable Temporal Language) — язык высокого уровня для программирования алгоритмов исследования графов BCG (определение функций на множествах состояний, реализация фиксированных точек для логик типа HML^[6], CTL^[7], ACTL^[8] и др.).

Связь между явными моделями (графы BCG) и неявными моделями (исследуемыми on-the-fly) обеспечивается совместимыми с OPEN/CAESAR компиляторами (CAESAR.OPEN, BCG.OPEN, EXP.OPEN, FSP.OPEN, LNT.OPEN, SEQ.OPEN).

В состав CADP также входят инструменты ALDEBARAN и TGV (Test Generation based on Verification), разработанные лабораторией Verimag (Гренобль) и проектной группой Vertecs INRIA Rennes.

Интеграция инструментов реализована с помощью графического интерфейса EUCALYPTUS и скриптового языка SVL^[9]. Оба средства объединяют доступ к инструментам CADP, автоматизируя преобразование форматов файлов и выбор нужных опций командной строки.

• В 2002 году Раду Мэческу, автор и разработчик модель-чекера EVALUATOR для CADP, был награждён премией Information Technology Award за вклад в симпозиуме Foundation Rhône-Alpes Futur^[10].

• В 2011 году Юбер Гаравель, архитектор и разработчик ПО CADP, получил премию Гей-Люссака — Гумбольдта^[11].

• В 2019 году Фредерик Ланг и Франко Маццанти заняли первые места во всех параллельных задачах конкурса RERS, используя CADP для правильной проверки 360 формул CTL и LTL на различных моделях коммуницирующих автоматов^[12].^[13]

• В 2020 году Фредерик Ланг, Франко Маццанти и Венделин Серве выиграли три золотые медали на конкурсе RERS’2020, правильно решив 88 % параллельных CTL-задач^[14].^[15][16]

• В 2021 году Юбер Гаравель, Фредерик Ланг, Раду Мэческу и Венделин Серве получили совместно приз «Инновация» от Inria — Академии наук — Dassault Systèmes за научный труд, приведший к созданию CADP^[17].

• В 2023 году Юбер Гаравель, Фредерик Ланг, Раду Мэческу и Венделин Серве получили за CADP первую премию Test-of-Time Tool Award от ETAPS, ведущего европейского форума по науке о программном обеспечении^[18].