FDR (программное обеспечение) - FDR (software)

FDR FDR2 FDR3 FDR4
Программное обеспечение для проверки уточнения FDR4 CSP logo.png
Разработчики)Оксфордский университет, Cocotec
Стабильный выпуск
4.2.4 / 19 февраля 2019; 21 месяц назад (2019-02-19)
Операционная система
  • GNU / Linux
  • MacOS
  • Windows
ТипCSP средство проверки уточнения
Лицензияпроприетарное программное обеспечение
Интернет сайтhttps://cocotec.io/fdr/

FDR (Уточнение отказов-расхождений) и впоследствии FDR2, FDR3 и FDR4 находятся уточнение проверка программные инструменты, предназначенный для проверки формальные модели выражено в Связь последовательных процессов (CSP). Инструменты изначально были разработаны Formal Systems (Europe) Ltd.[1] Билл Роско из Департамент компьютерных наук Оксфордского университета разработал многие алгоритмы, используемые инструментом и Майкл Голдсмит[2] сыграл важную роль в реализации.[3] FDR2 был разработан Департамент компьютерных наук Оксфордского университета откуда он был свободно доступен для академического и другого некоммерческого использования.[4]

FDR часто описывают как модель проверки, но технически уточнение checker, поскольку он преобразует два выражения процесса CSP в Помеченные переходные системы (LTS), а затем определяет, является ли один из процессов уточнением другого в пределах некоторого указанного семантическая модель (следы, сбои, сбои / расхождения и некоторые другие альтернативы).[5] FDR2 применяет различные пространство состояний алгоритмы сжатия для обработки LTS, чтобы уменьшить размер пространства состояний, которое необходимо исследовать во время проверки уточнения.

FDR2 прошел через множество выпусков, заменив более ранний инструмент, теперь называемый FDR1, в 1995 году. На смену ему пришла FDR3, полностью переписанная версия, включающая, помимо прочего, параллельное выполнение и встроенную проверку типов. FDR3 ​​выпущен Оксфордский университет, которая также выпустила FDR2 в период с 2008 по 2012 гг.[6] Аниматор ProBE CSP интегрирован в FDR3. Теперь ему на смену пришел FDR4. FDR4 доступен от Cocotec.[7]

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

  1. ^ Формальные Системы (Европа) Лтд..
  2. ^ Профессор Майкл Голдсмит (также сейчас из Оксфордского университета).
  3. ^ Филиппа Бродфут и Билл Роско. Учебник по FDR и его приложениям. Клаус Хавелунд, Джон Пеникс, Виллем Виссер (редакторы), Проверка модели SPIN и проверка программного обеспечения, Springer-Verlag, Конспект лекций по информатике, Том 1885, страница 322, 2000.
  4. ^ Программное обеспечение: FDR2, с коммерческими лицензиями, полученными от Формальные Системы (Европа) Лтд..
  5. ^ A.W. Роско (1994). «Модель-проверка CSP». В Классический разум: эссе в честь МАШИНА. Hoare. Prentice Hall. Цитировать журнал требует | журнал = (помощь)
  6. ^ Введение в FDR3
  7. ^ Программное обеспечение: FDR4, с коммерческими лицензиями, доступными после загрузки и первого запуска