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

CADP [1] ( Construction and Analysis of Distributed Processes ) — это набор инструментов для проектирования протоколов связи и распределенных систем. CADP разработан командой CONVECS (ранее командой VASY) в INRIA Rhone-Alpes и связан с различными дополнительными инструментами. CADP поддерживается, регулярно совершенствуется и используется во многих промышленных проектах.

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

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

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

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

История

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

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

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

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

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

Возможности 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 может описывать как асинхронные параллельные процессы, так и сложные структуры данных.

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

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

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

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

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

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

  • CAESAR.ADT [4] — компилятор, который транслирует абстрактные типы данных LOTOS в типы и функции C. Трансляция включает в себя методы компиляции с сопоставлением с образцом и автоматическое распознавание обычных типов (целые числа, перечисления, кортежи и т. д.), которые реализованы оптимально.
  • CAESAR [5] — это компилятор, который транслирует процессы LOTOS либо в код C (для быстрого прототипирования и тестирования), либо в конечные графы (для проверки). Трансляция выполняется с использованием нескольких промежуточных шагов, среди которых построение сети Петри, расширенной типизированными переменными, функциями обработки данных и атомарными переходами.
  • OPEN/CAESAR [6] — это общая программная среда для разработки инструментов, которые исследуют графы на лету (например, инструменты моделирования, проверки и генерации тестов). Такие инструменты могут быть разработаны независимо от любого конкретного языка высокого уровня. В этом отношении 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, которые позволяют проводить интерактивное моделирование
    • TERMINATOR, который ищет состояния тупика
  • 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 предоставляет примитивы для обработки состояний, переходов, меток, функций последователей и предшественников и т. д. Например, можно определить рекурсивные функции на наборах состояний, которые позволяют указать в 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 (Test Generation Based on Verification), разработанные лабораторией Verimag (Гренобль) и проектной группой Vertecs из INRIA в Ренне.

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


Награды

  • В 2002 году Раду Матееску, который спроектировал и разработал средство проверки моделей EVALUATOR для CADP, получил премию в области информационных технологий, присуждаемую на 10-м ежегодном симпозиуме, организованном Фондом Рона-Альпы Будущее. [11]
  • В 2020 году Фредерик Ланг, Франко Маццанти и Венделин Серве выиграли три золотые медали на соревновании RERS'2020, правильно решив 88% задач «Parallel CTL», дав ответы «не знаю» только для 11 формул из 90. [15] [16] [17]
  • В 2021 году Юбер Гаравель, Фредерик Ланг, Раду Матееску и Венделин Серве совместно выиграли премию за инновации Inria – Академии наук – Dassault Systèmes за свою научную работу, которая привела к разработке набора инструментов CADP. [18]
  • В 2023 году Юбер Гаравель, Фредерик Ланг, Раду Матееску и Венделин Серве совместно получили за набор инструментов CADP первую в истории премию Test-of-Time Tool Award от ETAPS , ведущего европейского форума по программной науке. [19]

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

Ссылки

  1. ^ Гаравел Х., Ланг Ф., Матееску Р., Серве В.: CADP 2011: набор инструментов для построения и анализа распределенных процессов. Международный журнал по программным инструментам для передачи технологий (STTT), 15(2):89-107, апрель 2013 г.
  2. ^ ISO 8807, Язык спецификации временного упорядочения
  3. ^ Форма онлайн-запроса CADP. Cadp.inria.fr (30.08.2011). Получено 16.06.2014.
  4. ^ H. Garavel. Compilation of LOTOS Abstract Data Types , в Трудах 2-й Международной конференции по методам формального описания FORTE'89 (Ванкувер, Британская Колумбия, Канада), ST Vuong (редактор), North-Holland, декабрь 1989 г., стр. 147–162.
  5. ^ H. Garavel, J. Sifakis. Compilation and Verification of LOTOS Specifications , в Трудах 10-го Международного симпозиума по спецификации протоколов, тестированию и верификации (Оттава, Канада), L. Logrippo, RL Probert, H. Ural (редакторы), North-Holland, IFIP, июнь 1990 г., стр. 379–394.
  6. ^ H. Garavel. OPEN/CÆSAR: Открытая архитектура программного обеспечения для верификации, моделирования и тестирования , в Трудах первой международной конференции по инструментам и алгоритмам для построения и анализа систем TACAS'98 (Лиссабон, Португалия), Берлин, B. Steffen (редактор), Lecture Notes in Computer Science, Полная версия доступна как Inria Research Report RR-3352, Springer Verlag, март 1998 г., т. 1384, стр. 68–84.
  7. ^ М. Хеннесси, Р. Милнер. Алгебраические законы недетерминизма и параллелизма , в: Журнал ACM , 1985, т. 32, стр. 137–161.
  8. ^ EM Clarke, EA Emerson, AP Sistla. Автоматическая проверка конечных параллельных систем с использованием спецификаций темпоральной логики , в: ACM Transactions on Programming Languages ​​and Systems , апрель 1986 г., т. 8, № 2, стр. 244–263.
  9. ^ Р. Де Никола, Ф. В. Ваандрагер. Логики, основанные на действии и состоянии, для систем переходов , Конспект лекций по информатике , Springer Verlag, 1990, т. 469, стр. 407–419.
  10. ^ H. Garavel, F. Lang. SVL: язык сценариев для композиционной верификации , в: Труды 21-й Международной конференции IFIP WG 6.1 по формальным методам для сетевых и распределенных систем FORTE'2001 (остров Чеджудо, Корея), M. Kim, B. Chin, S. Kang, D. Lee (редакторы), Полная версия доступна как Inria Research Report RR-4223, Kluwer Academic Publishers, IFIP, август 2001 г., стр. 377–392.
  11. ^ «Раду Матееску выигрывает премию в области информационных технологий, присуждаемую Фондом Рона-Альпы Футур» .
  12. ↑ Изабель Беллин (16 апреля 2011 г.). «Юбер Гаравель получил исследовательскую премию Гей-Люссака Гумбольдта». Архивировано из оригинала 2016-07-10.
  13. ^ «Результаты RERS Challenge 2019».
  14. ^ «Информационный бюллетень CADP № 12 — 10 апреля 2019 г.».
  15. ^ «Результаты RERS Challenge 2020».
  16. ^ «Команда CNR-Inria завоевала золотые медали на RERS 2020 Parallel CTL Challenge».
  17. ^ «Информационный бюллетень CADP № 13 — 22 февраля 2021 г.».
  18. ^ «Команда Convecs усиливает безопасность параллельных систем».
  19. ^ «Премия ETAPS за проверенный временем инструмент».
  • http://cadp.inria.fr/
  • http://vasy.inria.fr/
  • http://convecs.inria.fr/
Взято с "https://en.wikipedia.org/w/index.php?title=Построение_и_анализ_распределенных_процессов&oldid=1217241577"