Список инструментов проверки модели
В этой статье перечислены инструменты проверки моделей и дан обзор функциональности каждого из них.
Обзор некоторых инструментов проверки моделей [ править ]
В следующей таблице представлены средства проверки моделей, у которых есть
- веб-сайт, с которого его можно скачать,
- заявленная лицензия,
- описание, опубликованное в архивной литературе, и
- статья в Википедии, описывающая это.
В таблице ниже используются следующие сокращения:
- Эквиваленты:
- SB: Сильная бисимуляция
- ВБ: Слабая бисимуляция
- BB: Бисимуляция ветвления
- STE: сильная эквивалентность трассировки
- WTE: слабая эквивалентность трассировки
- я: Мэй Эквивалент
- Я: Должна быть эквивалентность
- OE: Наблюдательная эквивалентность
- SE: Эквивалент безопасности
- t*E: tau*.a Эквивалентность
- Лицензия на программное обеспечение:
- FUSC: бесплатно при определенных условиях (например, бесплатно для преподавателей).
| Имя | Проверка модели | Проверка эквивалентности | графический интерфейс | Доступность | |||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| Обычный, вероятностный, стохастический, ... | Язык моделирования | Язык свойств | Поддерживаемые эквиваленты | Генерация встречного примера | графический интерфейс | Графическая спецификация | Визуализация встречного примера | Лицензия на программное обеспечение | Используемый язык программирования | Платформа, ОС | |
| ВЗРЫВ | Анализ кода | С | Мониторные автоматы | Да | Нет | Нет | Нет | Бесплатно | OCaml | Windows, Unix-связанные | |
| КАПР | Простой и вероятностный | ЛОТОС , ФК2, ФСП, ЛНТ | АФМК, MCL, XTL | SB, WB, BB, OE, STE, WTE, SE, цена*E | Да | Да | Нет | Да | ФСК | C , оболочка Борна , Tcl / Tk , LOTOS , LNT | macOS, Linux, Солярис , Windows |
| CPAchecker | Анализ кода | С | Мониторные автоматы | Да | Да | Нет | Да | Бесплатно | Ява | Любой | |
| МЕЧТАТЬ | В режиме реального времени | C++ , Автоматы с таймером | Мониторные автоматы | Да | Нет | Нет | Нет | Бесплатно | С++ | Windows, Unix-связанные | |
| Java-следопыт | Просто и по времени | Ява | неизвестный | Нет | Да | Нет | Нет | Соглашение об открытом исходном коде | Ява | macOS, Windows, Linux | |
| Мурфи (Мерфи) | Простой | Мурφ | Инварианты, утверждения | Да | Нет | Нет | Нет | Бесплатно | С++ | Линукс | |
| НуСМВ | Простой | Язык ввода SMV | CTL , LTL , PSL | Да | Нет | Нет | Нет | Бесплатно | С | Юникс, Windows, macOS | |
| ПАТ | Обычный, в реальном времени, вероятностный | CSP# , CSP по времени, вероятностный CSP | LTL , утверждения | Да | Да | Да | Да | Бесплатно | С# | Windows, другие с Mono | |
| ПРИЗМА | Вероятностный | PEPA , язык PRISM, Plain MC | CSL, PLTL, PCTL | Нет | Да | Нет | Нет | Бесплатно | С++ , Ява | Виндовс, Линукс, МакОС | |
| Слухи | Простой | Мурφ | Инварианты, утверждения | Да | Нет | Нет | Нет | Бесплатно | С | макОС, Линукс | |
| ВРАЩАТЬСЯ | Простой | Promela | литы | Да | Да | Нет | Да | ФСК | С , С++ | Windows, Unix-связанные | |
| ТАПААЛ | В режиме реального времени | Сети Петри с временной дугой, возрастные инварианты, ингибиторные дуги, транспортные дуги | Подмножество TCTL | Нет | Да | Да | Да | Бесплатно | С++ , Ява | macOS, Windows, Linux | |
| ТАПА | Простой | CCSP | CTL , μ-исчисление | SB, WB, BB, STE, WTE, я, ME, OE | Да | Да | Да | Да | Бесплатно | Ява | Windows, macOS, Unix-связанные |
| УПААЛ | В режиме реального времени | Автоматы с таймером , подмножество C | Подмножество TCTL | Да | Да | Да | Да | ФСК | С++ , Ява | macOS, Windows, Linux | |
| РОМЕО | В режиме реального времени | Временные сети Петри, параметрические сети Петри с секундомером | Подмножество TCTL | Да | Да | Да | Нет | Бесплатно | С++ , Tcl / Tk | macOS, Windows, Linux | |
| Средство проверки модели TLA+ (TLC) | Простой | TLA+ , ПлюсКал | ПРИХОДИТЬ | Да | Да | Да | Нет | Бесплатно | Ява | macOS, Windows, Linux | |
Языки моделирования [ править ]
- CCSP: исчисление процессов, полученное из CCS путем включения некоторых операторов CSP . Это определено Олдерогом [1] и ван Глаббек/Ваандрагер. [2]
- CSP : обмен информацией о последовательных процессах; формальный язык для описания закономерностей взаимодействия в параллельных системах. FDR2 — это инструмент уточнения CSP, сравнивающий две модели на предмет совместимости.
- Язык ввода DVE: система описывается как сеть расширенных конечных автоматов, взаимодействующих через общие переменные и небуферизованные каналы. Не содержит поддержки буферизованных каналов и проверки типа получаемого сообщения без выполнения самого приема.
- FC2: (Common Format V2) Представление ASCII на машинном уровне для синхронизированных (иерархических) сетей автоматов. Определен Esprit Basic Research Action CONCUR, 1992. Используется в качестве формата ввода и обмена рядом инструментов проверки, в основном в области алгебр процессов.
- FSP: язык процессов с конечным состоянием, определенный в Имперском колледже.
- Java : объектно-ориентированный язык программирования.
- LNT: Новые технологии LOTOS; язык спецификаций, вдохновленный исчислением процессов, функциональными языками программирования и императивными языками программирования; LNT был разработан как современная замена LOTOS и E-LOTOS .
- LOTOS : Спецификация языка временного упорядочения (стандарт ISO 8807); язык формальной спецификации, основанный на временном упорядочении, используемый для спецификации протокола в стандартах ISO OSI.
- mCRL2 : язык спецификации для описания параллельных систем дискретных событий.
- Murφ : защищенные команды и асинхронная чередующаяся модель параллелизма, при которой вся синхронизация и связь осуществляются через глобальные переменные.
- PEPA : Алгебра процесса оценки эффективности; это алгебра стохастических процессов, предназначенная для моделирования компьютерных и коммуникационных систем.
- Обычный MC: простые форматы текстовых файлов, используемые в MRMC и PRISM.
- Promela : метаязык процесса или протокола; это язык моделирования проверки. Язык позволяет динамически создавать параллельные процессы для моделирования, например, распределенных систем.
- TLA+ : язык спецификации общего назначения, основанный на временной логике действий, первоначально использовавшийся для распределенных и параллельных систем. Язык спецификаций и их свойств один и тот же.
Язык свойств [ изменить ]
- без альтернаций AFMC: модальное μ-исчисление .
- Утверждения : императивные утверждения-утверждения.
- CSL: Непрерывная стохастическая логика, характеризует бисимуляцию марковских процессов с непрерывным временем.
- CSRL: непрерывная стохастическая логика вознаграждения; логика для определения мер над CTMC, расширенная структурой вознаграждения (так называемые модели вознаграждения Маркова).
- CTL : логика дерева вычислений; логика ветвления времени, означающая, что ее модель времени представляет собой древовидную структуру, в которой будущее не определено; в будущем существуют разные пути, любой из которых может оказаться реальным и реализованным путем.
- Инварианты : предикаты состояния системы.
- LTL : Линейная временная логика; модальная темпоральная логика с модальностями, относящимися ко времени.
- MCL: язык проверки модели; без альтернатив, Модальное μ-исчисление дополненное удобными для пользователя регулярными выражениями и конструкциями передачи значений; включает CTL и LTL .
- mCRL2 Козена мю-исчисление: пропозициональное модальное мю-исчисление (исключая атомарные предложения), расширенное за счет: процессов, зависящих от данных, количественной оценки типов данных, множественных действий, времени и регулярных формул.
- PCTL : Вероятностный CTL ; расширение CTL, которое позволяет проводить вероятностную количественную оценку описанных свойств.
- PLTL: Вероятностная линейная временная логика.
- 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) сравнивает производительность инструментов проверки моделей, предназначенных для анализа высококонкурентных систем.
См. также [ править ]
Ссылки [ править ]
- ^ ER Olderog : Операционная семантика сети Петри для CCSP
- ^ Роб ван Глаббек, Фриц Ваандрагер: Структуры событий пакета и CCSP
- ^ Ромейн, Джуди (июнь 1999 г.). Модель проверки протокола выборов лидера HAVi (технический отчет). Амстердам: КРИ. СЕН-Р9915. Архивировано из оригинала 11 сентября 2019 г. Проверено 14 июня 2018 г.
- ^ Донг, Ифэй; Ду, Сяоцюнь; Хольцманн, Жерар; Смолка, Скотт (2003). «Борьба с Livelock в GNU i-протоколе: пример проверки модели с явным состоянием». Программный инструмент для трансфера технологий . 4 (4): 505–528.
- ^ Бортник Елена Михайловна; Трчка, Никола; Вейс, Антон; Люттик, Бас; ван де Мортель-Фрончак, JM; Баетен, Джос КМ; Фоккинк, Ван; Руда, Дж. Э. (2005). «Анализ модели ци системы проигрывателя с использованием Spin, CADP и Uppaal» (PDF) . Журнал логических и алгебраических методов программирования . 65 (2): 51–104. дои : 10.1016/j.jlap.2005.05.001 . Архивировано (PDF) из оригинала 27 января 2021 г. Проверено 25 мая 2018 г.
- ^ Маццанти, Франко; Феррари, Алессио (2018). «Десять разнообразных формальных моделей для автоматической системы наблюдения за поездами CBTC». Материалы 3-го семинара по моделям формального анализа реальных систем и 6-го международного семинара по верификации и трансформации программ (MARS/VPT'18), Салоники, Греция . Электронные труды по теоретической информатике. Том. 268. стр. 104–149. arXiv : 1803.10324v1 . дои : 10.4204/EPTCS.268.4 .
Внешние ссылки [ править ]
- Инструменты : база данных для инструментов проверки.
- Список инструментов проверки и синтеза (публичный репозиторий на GitHub)
- Список инструментов проверки вероятностных, стохастических, гибридных и временных систем.
- Общие критерии