Список инструментов проверки моделей

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

Обзор некоторых инструментов проверки моделей

В следующей таблице приведены средства проверки моделей, которые имеют

1. веб-сайт, с которого его можно скачать,
2. заявленная лицензия,
3. описание, опубликованное в архивной литературе, и
4. Статья в Википедии, описывающая это.

В таблице ниже используются следующие сокращения:

• Эквивалентности:
  • SB: Сильная бисимуляция
  • WB: Слабая бисимуляция
  • BB: Бисимуляция ветвления
  • STE: Сильная эквивалентность следов
  • WTE: Слабая эквивалентность следов
  • я: Май Эквивалентность
  • МЭ: Должна быть эквивалентна
  • OE: Наблюдаемая эквивалентность
  • SE: Эквивалентность безопасности
  • t*E: tau*.a Эквивалентность
• Лицензия на программное обеспечение:
  • FUSC: Бесплатно при определенных условиях (например, бесплатно для ученых)

Языки моделирования

• CCSP: Исчисление процесса, полученное из CCS путем включения некоторых операторов CSP . Определено Олдерогом ^[1] и ван Глаббеком/Ваандрагером. ^[2]
• CSP : Коммуникационные последовательные процессы; формальный язык для описания моделей взаимодействия в параллельных системах. FDR2 — это инструмент проверки уточнений для CSP, сравнивающий две модели на совместимость.
• Язык ввода DVE: система описывается как сеть расширенных конечных автоматов, взаимодействующих через общие переменные и небуферизованные каналы. Не содержит поддержки буферизованных каналов и проверки типа сообщения, которое должно быть получено, без выполнения собственно приема.
• FC2: (Common Format V2) Представление ASCII на уровне машины для синхронизированных (иерархических) сетей автоматов. Определено Esprit Basic Research Action CONCUR, 1992. Используется в качестве входного и обменного формата рядом инструментов верификации, в основном в области алгебр процессов.
• FSP: язык конечных процессов, определенный в Имперском колледже.
• Java : объектно-ориентированный язык программирования.
• LNT: LOTOS New Technology; язык спецификаций, вдохновленный исчислением процессов, языками функционального программирования и императивными языками программирования; LNT был разработан как современная замена LOTOS и E-LOTOS .
• LOTOS : Язык спецификации временного упорядочения (стандарт ISO 8807); формальный язык спецификаций, основанный на временном упорядочении, используемый для спецификации протоколов в стандартах ISO OSI.
• mCRL2 : язык спецификаций для описания систем параллельных дискретных событий.
• Murφ : защищенные команды и асинхронная, чередующаяся модель параллелизма, при этом вся синхронизация и связь осуществляются через глобальные переменные.
• PEPA : Алгебра процессов оценки производительности; это алгебра стохастических процессов, предназначенная для моделирования компьютерных и коммуникационных систем.
• Plain MC: простые форматы текстовых файлов, используемые в MRMC и PRISM.
• Promela : метаязык процессов или протоколов; это язык моделирования проверки. Язык позволяет динамически создавать параллельные процессы для моделирования, например, распределенных систем.
• TLA+ : Язык спецификаций общего назначения, основанный на Временной Логике Действий, изначально использовавшийся для распределенных и параллельных систем. Язык спецификаций и их свойств тот же.

Свойства языка

• AFMC: Модальное μ-исчисление без чередования .
• Утверждения : Повелительные утверждения.
• CSL: Непрерывная стохастическая логика, характеризует бисимуляцию непрерывных во времени марковских процессов.
• CSRL: Непрерывная стохастическая логика вознаграждения; логика для определения мер по CTMC, расширенная структурой вознаграждения (так называемые модели вознаграждения Маркова).
• CTL : Логика дерева вычислений; логика с разветвленным временем, означающая, что ее модель времени представляет собой древовидную структуру, в которой будущее не определено; в будущем существуют различные пути, любой из которых может быть фактическим путем, который будет реализован.
• Инварианты : Предикаты состояния системы.
• LTL : Линейная временная логика; модальная временная логика с модальностями, относящимися ко времени.
• MCL: Язык проверки моделей; Модальное μ-исчисление без чередования, расширенное удобными для пользователя регулярными выражениями и конструкциями передачи значений; включает CTL и LTL .
• mCRL2 mu-исчисление: пропозициональное модальное μ-исчисление Козена (исключая атомарные предложения), расширенное: процессами, зависящими от данных, квантификацией по типам данных, многодействиями, временем и обычными формулами.
• PCTL : Вероятностный CTL ; расширение CTL, которое позволяет проводить вероятностную количественную оценку описываемых свойств.
• ПЛВЛ: Вероятностная линейная временная логика.
• PRCTL: Логика дерева вычисления вероятностного вознаграждения; расширяет PCTL свойствами, ограниченными вознаграждением.
• PSL : Язык спецификации свойств
• SVA: подмножество языка утверждений стандартов SystemVerilog , стандартизированное как IEEE 1800
• XTL: расширенный темпоральный язык; предметно-ориентированный язык для быстрой реализации основанных на действиях, явных состояниях и передаче значений проверок моделей.

Сравнение инструментов проверки моделей

Научные публикации

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

• В 1999 году Джуди Ромейн сравнила два средства проверки моделей ( CADP и SPIN ) на предмет совместимости аудио-видео протокола HAVi для бытовой электроники. ^[3]

• В 2003 году Ифэй Дун, Сяоцюнь Ду, Джерард Дж. Хольцманн и Скотт А. Смолка опубликовали сравнение четырех программ проверки моделей (а именно: Cospan, Murphi , SPIN и XMC) на протоколе связи GNU i-protocol. ^[4]

• В 2005 году Елена М. Бортник, Никола Трчка, Антон Вийс, Бас Люттик, Дж. М. ван де Мортель-Фрончак, Йос К. М. Баетен, Ван Фоккинк и Дж. Е. Руда опубликовали сравнение четырех моделей проверочных программ (а именно: CADP , muCRL, SPIN , и UPPAAL ) на промышленной производственной системе — вращающемся сверлильном станке. ^[5]

• В 2018 году Ф. Маццанти и А. Феррари опубликовали сравнение десяти средств проверки моделей (а именно: CADP , CPN Tools, FDR4, NuSMV /nuXmv, mCRL2 , ProB, SPIN , TLA+ , UMC и UPPAAL ) по проблеме контроля движения поездов, принимая во внимание как удобство использования языков, так и производительность инструментов. ^[6]

Международные конкурсы программного обеспечения

• С 2007 года Конкурс по проверке моделей оборудования (HWMCC) сравнивает производительность инструментов проверки моделей, ориентированных на проектирование оборудования.
• С 2011 года в рамках конкурса по проверке моделей (MCC) сравниваются показатели инструментов проверки моделей, предназначенных для анализа высококонкурентных систем.

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

• AltaRica

Ссылки

1. ER Olderog : Оперативная семантика сети Петри для CCSP
2. Роб ван Глаббек, Фриц Ваандрагер: Структуры событий пакета и CCSP
3. Romijn, Judi (июнь 1999). Model Checking a HAVi Leader Election Protocol (технический отчет). Амстердам: CWI. SEN-R9915. Архивировано из оригинала 2019-09-11 . Получено 2018-06-14 .
4. Дун, Ифэй; Ду, Сяоцюнь; Хольцманн, Джерард; Смолка, Скотт (2003). «Борьба с динамической блокировкой в ​​протоколе GNU i: исследование случая проверки модели явного состояния». Программный инструмент для передачи технологий . 4 (4): 505–528.
5. Бортник, Елена М.; Трчка, Никола; Вийс, Антон; Люттик, Бас; ван де Мортель-Фрончак, Дж. М.; Батен, Йос К. М.; Фоккинк, Ван; Руда, Дж. Э. (2005). «Анализ модели хи системы поворотного стола с использованием Spin, CADP и Uppaal» (PDF) . Журнал логических и алгебраических методов в программировании . 65 (2): 51–104. doi : 10.1016/j.jlap.2005.05.001 . Архивировано (PDF) из оригинала 27.01.2021 . Получено 25.05.2018 .
6. Mazzanti, Franco; Ferrari, Alessio (2018). «Десять различных формальных моделей для системы автоматического контроля за движением поездов CBTC». Труды 3-го семинара по моделям для формального анализа реальных систем и 6-го международного семинара по верификации и преобразованию программ (MARS/VPT'18), Салоники, Греция . Электронные труды по теоретической информатике. Том 268. С. 104–149. arXiv : 1803.10324v1 . doi :10.4204/EPTCS.268.4.

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

• Инструменты: база данных для инструментов проверки
• Список инструментов проверки и синтеза (публичный репозиторий на GitHub)
• Список инструментов проверки вероятностных, стохастических, гибридных и временных систем

Общие контрольные показатели

• MCC (модели конкурса проверки моделей): коллекция сотен сетей Петри, созданных на основе множества академических и промышленных исследований.
• VLTS (Very Large Transition Systems): набор маркированных переходных систем увеличивающихся размеров, используемых во многих научных публикациях.