Построение и анализ распределенных процессов - Construction and Analysis of Distributed Processes

Построение и анализ распределенных процессов
Cadp logo.gif
Разработчики)INRIA CONVECS команда (ранее ВАСИ команда)
изначальный выпуск1989, 30–31 год назад
Стабильный выпуск
2018/13 декабря 2018; 23 месяца назад (2018-12-13)
Операционная системаWindows, macOS, Linux, Солярис, и OpenIndiana
ТипНабор инструментов для проектирования коммуникационных протоколов и распределенных систем
Интернет сайтcadp.inria.fr

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

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

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

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

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

История

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

Основные выпуски

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

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

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

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

CADP предлагает широкий набор функций, от пошагового моделирования до массового параллелизма. проверка модели. Это включает в себя:

  • Компиляторы для нескольких формализмов ввода:
    • Описание протоколов высокого уровня, написанное на языке ISO LOTOS.[2] Набор инструментов содержит два компилятора (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, заполните регистрационную форму по адресу.[3] После подписания лицензионного соглашения вы получите подробную информацию о том, как загрузить и установить CADP.

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

Набор инструментов содержит несколько инструментов:

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

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

    • БИСИМУЛЯТОР, который проверяет эквивалентность бисимуляции и предварительные заказы
    • CUNCTATOR, который выполняет имитацию установившегося состояния на лету
    • ДЕТЕРМИНАТОР, который устраняет стохастический недетерминизм в нормальных, вероятностных или стохастических системах
    • ДИСТРИБЬЮТОР, формирующий граф достижимых состояний на нескольких машинах.
    • EVALUATOR, который оценивает обычные формулы мю-исчисления без чередования
    • ИСПОЛНИТЕЛЬ, который выполняет произвольное выполнение кода
    • EXHIBITOR, который ищет последовательности выполнения, соответствующие заданному регулярному выражению.
    • ГЕНЕРАТОР, который строит граф достижимых состояний
    • PREDICTOR, которые позволяют прогнозировать выполнимость анализа достижимости,
    • ПРОЕКТОР, который вычисляет абстракции коммуникационных систем.
    • РЕДУКТОР, который строит и минимизирует граф достижимых состояний по модулю различных отношений эквивалентности.
    • SIMULATOR, X-SIMULATOR и OCIS, которые позволяют интерактивное моделирование
    • ТЕРМИНАТОР, который ищет состояния тупика
  • BCG (Binary Coded Graphs) - это как формат файла для хранения очень больших графиков на диске (с использованием эффективных методов сжатия), так и программная среда для обработки этого формата, включая графы разбиения для распределенной обработки. 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 предоставляет примитивы для обработки состояний, переходов, меток, функций-преемников и предшественников и т.д. как HML,[7] CTL,[8] ACTL,[9] так далее.).

Связь между явными моделями (такими как графы 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 Rennes.

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

Смотрите также

  • СИНТАКСИС генератор компилятора (используется для сборки многих CADP составители и переводчики)

Рекомендации

  1. ^ Гаравел Х, Ланг Ф, Матееску Р, Серве В: CADP 2011: набор инструментов для построения и анализа распределенных процессов Международный журнал программных средств для передачи технологий (STTT), 15 (2): 89-107, апрель 2013 г.
  2. ^ ISO 8807, Язык спецификации временного упорядочивания
  3. ^ Форма онлайн-запроса CADP. Cadp.inria.fr (30 августа 2011 г.). Проверено 16 июня 2014.
  4. ^ Х. Гаравел. Составление абстрактных типов данных LOTOS, в Материалы 2-й Международной конференции по методам формального описания FORTE'89 (Ванкувер, Британская Колумбия, Канада), С. Т. Вуонг (редактор), Северная Голландия, декабрь 1989 г., стр. 147–162.
  5. ^ Х. Гаравел, Дж. Сифакис. Составление и проверка спецификаций LOTOS, в Материалы 10-го Международного симпозиума по спецификации, тестированию и проверке протоколов (Оттава, Канада), Л. Логриппо, Р. Л. Проберт, Х. Урал (редакторы), Северная Голландия, ИФИП, июнь 1990 г., стр. 379–394.
  6. ^ Х. Гаравел. OPEN / CÆSAR: открытая программная архитектура для проверки, моделирования и тестирования, in Proceedings of the First International Conference on Tools and Algorithms for Construction TACAS'98 (Лиссабон, Португалия), Берлин, Б. Штеффен (редактор), Lecture Notes in Computer Science, Полная версия доступна как Отчет об исследованиях Inria RR-3352, Springer Verlag, март 1998 г., т. 1384, стр. 68–84.
  7. ^ М. Хеннесси, Р. Милнер. Алгебраические законы недетерминизма и параллелизма, в: Журнал ACM, 1985, т. 32, стр. 137–161.
  8. ^ Э. М. Кларк, Э. А. Эмерсон, А. П. Систла. Автоматическая проверка одновременных систем с конечным числом состояний с использованием спецификаций временной логики, в: Транзакции ACM по языкам и системам программирования, Апрель 1986, т. 8, № 2, с. 244–263.
  9. ^ Р. Де Никола, Ф. В. Ваандрагер. Действие против логики на основе состояний для переходных систем, Конспект лекций по информатике, Springer Verlag, 1990, т. 469, стр. 407–419.
  10. ^ Х. Гаравел, Ф. Ланг.SVL: язык сценариев для проверки композиции, в: Материалы 21-й Международной конференции IFIP WG 6.1 по формальным методам для сетевых и распределенных систем FORTE'2001 (Остров Чеджу, Корея), М. Ким, Б. Чин, С. Кан, Д. Ли (редакторы), Полная версия доступна как Отчет об исследованиях Inria RR-4223, Kluwer Academic Publishers, IFIP, август 2001 г., стр. 377–392.

внешняя ссылка