Построение и анализ распределенных процессов

Построение и анализ распределенных процессов

Разработчик(и)	Команда ИНРИА КОНВЕКС (ранее ВАСИ ) команда
Первоначальный выпуск	1989 г., 34–35 лет назад.
Стабильная версия	2023 год / 13 февраля 2023 г ( 13.02.2023 )
Операционная система	Windows , macOS , Linux , Solaris и OpenIndiana
Тип	Инструментарий для проектирования протоколов связи и распределенных систем
Веб-сайт	кадп .инрия .fr

КАПР ( Построение и анализ распределенных процессов ) — набор инструментов для проектирования протоколов связи и распределенных систем. CADP разработан командой CONVECS (ранее командой VASY) в INRIA Рона-Альпы и подключен к различным дополнительным инструментам. CADP поддерживается, регулярно совершенствуется и используется во многих промышленных проектах.

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

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

CADP включает инструменты для поддержки использования двух подходов в формальных методах, оба из которых необходимы для проектирования надежных систем:

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

История

Работа над CADP началась в 1986 году, когда была предпринята разработка первых двух инструментов — CAESAR и ALDEBARAN. В 1989 году была придумана аббревиатура CADP, которая расшифровывалась как CAESAR/ALDEBARAN Distribution Package . Со временем было добавлено несколько инструментов, в том числе программные интерфейсы, которые позволяли использовать инструменты: аббревиатура CADP затем стала пакетом разработки CAESAR/ALDEBARAN . В настоящее время CADP содержит более 50 инструментов. Несмотря на сохранение той же аббревиатуры, название набора инструментов было изменено, чтобы лучше отражать его назначение: Построение и анализ распределенных процессов .

Основные релизы

Релизы CADP последовательно обозначались буквами алфавита (от «А» до «Z»), затем названиями городов, в которых размещаются академические исследовательские группы, активно работающие над языком LOTOS , и, в более общем плане, названиями городов, в которых основные вклад в теорию параллелизма был сделан .

Кодовое имя	Дата
«А»… «З»	Январь 1990 г. - декабрь 1996 г.
Твенте	июнь 1997 г.
Льеж	Январь 1999 г.
Оттава	июль 2001 г.
Эдинбург	декабрь 2006 г.
Цюрих	декабрь 2013 г.
Амстердам	декабрь 2014 г.
Стоуни Брук	декабрь 2015 г.
Оксфорд	декабрь 2016 г.
София Антиполис	декабрь 2017 г.
Уппсала	декабрь 2018 г.
Пиза	декабрь 2019 г.
Ольборг	декабрь 2020 г.
Саарбрюккен	декабрь 2021 г.
Киста	декабрь 2022 г.
Ахен	февраль 2023 г.

Между основными выпусками часто доступны второстепенные выпуски, обеспечивающие ранний доступ к новым функциям и улучшениям. Для получения дополнительной информации см. страницу списка изменений на веб-сайте CADP.

Возможности CADP

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

• Компиляторы для нескольких входных формализмов:
  • Описания протоколов высокого уровня, написанные на языке ISO LOTOS . В набор инструментов входят два компилятора (CAESAR и CAESAR.ADT), которые преобразуют описания LOTOS в код C для использования в целях моделирования, проверки и тестирования.
  • Описания протоколов низкого уровня, заданные как конечные автоматы.
  • Сети взаимодействующих автоматов, т. е. конечные автоматы, работающие параллельно и синхронизированные (либо с использованием операторов алгебры процессов, либо с использованием векторов синхронизации).
• Несколько инструментов проверки эквивалентности (минимизация и сравнение по модулю отношений бисимуляции), такие как BCG_MIN и BISIMULATOR.
• Несколько средств проверки моделей для различной темпоральной логики и мю-исчисления, таких как EVALUATOR и XTL.
• Комбинировано несколько алгоритмов проверки: перечислительная проверка, оперативная проверка, символьная проверка с использованием бинарных диаграмм решений, композиционная минимизация, частичные заказы, проверка распределенной модели и т. д.
• Плюс другие инструменты с расширенными функциями, такими как визуальная проверка , оценка производительности и т. д.

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

Модели и методы проверки

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

Большинство алгоритмов проверки в CADP основаны на модели помеченных переходных систем (или просто автоматов или графов), которая состоит из набора состояний, начального состояния и отношения перехода между состояниями. Эта модель часто создается автоматически на основе высокоуровневых описаний изучаемой системы, а затем сравнивается со свойствами системы с использованием различных процедур принятия решений. В зависимости от формализма, используемого для выражения свойств, возможны два подхода:

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

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

• Маленькие модели можно представлять явно, сохраняя в памяти все их состояния и переходы (исчерпывающая проверка);
• Более крупные модели представляются неявно, путем изучения только состояний модели и переходов, необходимых для проверки (проверка на лету).

Языки

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

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

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

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

Лицензирование и установка

CADP распространяется бесплатно среди университетов и государственных исследовательских центров. Промышленные пользователи могут получить оценочную лицензию для некоммерческого использования в течение ограниченного периода времени, после чего потребуется полная лицензия. Чтобы запросить копию CADP, заполните регистрационную форму по адресу. После подписания лицензионного соглашения вы получите подробную информацию о том, как загрузить и установить CADP.

Обзор инструментов

В наборе инструментов имеется несколько инструментов:

• ЦЕЗАРЬ.ADT — это компилятор, который преобразует абстрактные типы данных LOTOS в типы C и функции C. Трансляция включает методы компиляции по шаблону и автоматическое распознавание обычных типов (целые числа, перечисления, кортежи и т. д.), которые реализованы оптимально.
• ЦЕЗАРЬ — это компилятор, который преобразует процессы LOTOS либо в код C (для быстрого прототипирования и тестирования), либо в конечные графы (для проверки). Трансляция выполняется с использованием нескольких промежуточных шагов, среди которых построение сети Петри, расширенной типизированными переменными, функциями обработки данных и атомарными переходами.
• ОТКРЫТЫЙ/ЦЕЗАРЬ — это общая программная среда для разработки инструментов, которые исследуют графики «на лету» (например, инструменты моделирования, проверки и создания тестов). Такие инструменты можно разрабатывать независимо от какого-либо конкретного языка высокого уровня. В этом отношении OPEN/CAESAR играет центральную роль в CADP, соединяя языко-ориентированные инструменты с модельно-ориентированными инструментами. OPEN/CAESAR состоит из набора из 16 библиотек кода со своими программными интерфейсами, такими как:
  • Caesar_Hash, содержащий несколько хеш-функций.
  • Caesar_Solve, который решает системы логических уравнений на лету.
  • Caesar_Stack, который реализует стеки для поиска в глубину.
  • Caesar_Table, который обрабатывает таблицы состояний, переходов, меток и т. д.

В среде OPEN/CAESAR был разработан ряд инструментов:

• • BISIMULATOR, который проверяет эквивалентность бисимуляции и предварительные заказы.
  • CUNCTATOR, который выполняет моделирование устойчивого состояния «на лету».
  • ДЕТЕРМИНАТОР, который устраняет стохастический недетерминизм в нормальных, вероятностных или стохастических системах.
  • ДИСТРИБЬЮТОР, который генерирует граф достижимых состояний с помощью нескольких машин.
  • EVALUATOR, который оценивает обычные формулы мю-исчисления без чередования.
  • EXECUTOR, выполняющий случайное выполнение кода.
  • EXHIBITOR, который ищет последовательности выполнения, соответствующие заданному регулярному выражению.
  • ГЕНЕРАТОР, строящий граф достижимых состояний
  • ПРЕДИКТОР, который прогнозирует осуществимость анализа достижимости,
  • ПРОЕКТОР, который вычисляет абстракции взаимодействующих систем.
  • РЕДУКТОР, который строит и минимизирует граф достижимых состояний по модулю различных отношений эквивалентности.
  • SIMULATOR, X-SIMULATOR и OCIS, которые позволяют интерактивное моделирование.
  • ТЕРМИНАТОР, который ищет тупиковые состояния
• BCG (двоично-кодированные графики) — это одновременно формат файла для хранения очень больших графов на диске (с использованием эффективных методов сжатия) и программная среда для обработки этого формата, включая разделение графов для распределенной обработки. BCG также играет ключевую роль в CADP, поскольку многие инструменты используют этот формат для своих входных/выходных данных. Среда BCG состоит из различных библиотек с их программными интерфейсами и нескольких инструментов, в том числе:
  • BCG_DRAW, который создает двумерное представление графика,
  • BCG_EDIT, который позволяет в интерактивном режиме изменять макет графика, созданный Bcg_Draw.
  • BCG_GRAPH, который генерирует различные формы практически полезных графиков.
  • BCG_INFO, отображающий различную статистическую информацию о графике.
  • BCG_IO, который выполняет преобразования между BCG и многими другими форматами графиков.
  • BCG_LABELS, который скрывает и/или переименовывает (с использованием регулярных выражений) метки перехода графа.
  • BCG_MERGE, который собирает фрагменты графа, полученные в результате построения распределенного графа.
  • BCG_MIN, который минимизирует граф по модулю сильных или ветвящихся эквивалентностей (а также может работать с вероятностными и стохастическими системами)
  • BCG_STEADY, который выполняет стационарный численный анализ (расширенных) цепей Маркова с непрерывным временем.
  • BCG_TRANSIENT, который выполняет переходный численный анализ (расширенных) цепей Маркова с непрерывным временем.
  • PBG_CP, который копирует разделенный граф BCG.
  • PBG_INFO, отображающий информацию о секционированном графе BCG.
  • PBG_MV, который перемещает разделенный граф BCG.
  • PBG_RM, который удаляет разделенный граф BCG.
  • XTL (eXecutable Temporal Language), который представляет собой функциональный язык высокого уровня для программирования алгоритмов исследования на графах BCG. XTL предоставляет примитивы для обработки состояний, переходов, меток, функций-преемников и предшественников и т. д. Например, можно определить рекурсивные функции для наборов состояний, что позволяет указывать в алгоритмах оценки и генерации диагностики XTL для обычных темпоральных логик (таких как как ХМЛ, СТЛ, АКТЛ, и т. д.).

Связь между явными моделями (такими как графики BCG) и неявными моделями (исследуемыми на лету) обеспечивается компиляторами, совместимыми с OPEN/CAESAR, включая:

• • CAESAR.OPEN, для моделей, выраженных в описаниях LOTOS.
  • BCG.OPEN, для моделей, представленных в виде графиков BCG.
  • EXP.OPEN, для моделей, выраженных как взаимодействующие автоматы.
  • FSP.OPEN, для моделей, выраженных в виде описаний FSP.
  • LNT.OPEN, для моделей, выраженных в виде описаний LNT.
  • SEQ.OPEN, для моделей, представленных в виде наборов трассировок выполнения.

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

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

Награды

• В 2002 году Раду Матееску, который спроектировал и разработал программу проверки модели EVALUATOR для CADP, получил премию в области информационных технологий, присуждаемую во время 10-го ежегодного симпозиума, организованного Фондом Рона-Альпы Футур.

• В 2011 году Хьюберт Гаравель, архитектор программного обеспечения и разработчик CADP, получил премию Гей-Люссака Гумбольдта .

• В 2019 году Фредерик Ланг и Франко Маццанти выиграли все золотые медали за параллельные задачи задачи RERS, используя CADP для успешной и правильной оценки формул 360-градусной вычислительной древовидной логики (CTL) и линейной временной логики (LTL) на различных наборах состояний связи. машины.

• В 2020 году Фредерик Ланг, Франко Маццанти и Венделин Серве выиграли три золотые медали на конкурсе RERS'2020, правильно решив 88% задач «Параллельный CTL», дав ответы «не знаю» только на 11 формул из 90. .

• В 2021 году Юбер Гаравель, Фредерик Ланг, Раду Матееску и Венделин Серве совместно выиграли премию за инновации Inria – Академии наук – Dassault Systèmes за свою научную работу, которая привела к разработке набора инструментов CADP.

• В 2023 году Юбер Гаравель, Фредерик Ланг, Раду Матееску и Венделин Серве совместно получили за набор инструментов CADP первую в истории награду «Испытание инструмента» от ETAPS , главного европейского форума по науке о программном обеспечении.

См. также

• Генератор компилятора SYNTAX (используется для создания многих CADP ) компиляторов и трансляторов

Внешние ссылки

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