ФДР (программное обеспечение)
 | |
| Разработчик(и) | Оксфордский университет , Кокотек |
|---|---|
| Стабильная версия | 4.2.4 / 19 февраля 2019 г |
| Операционная система |
|
| Тип | CSP Средство проверки уточнений |
| Лицензия | проприетарное программное обеспечение |
| Веб-сайт | https://cocotec.io/fdr/ |
FDR ( Уточнение ошибок-расхождений ), а затем FDR2 , FDR3 и FDR4 — это уточнений проверки программные инструменты , предназначенные для проверки формальных моделей, выраженных в коммуникативных последовательных процессах (CSP). Первоначально эти инструменты были разработаны компанией Formal Systems (Europe) Ltd. [1] Билл Роско с факультета компьютерных наук Оксфордского университета разработал многие алгоритмы, используемые этим инструментом, а Майкл Голдсмит [2] сыграл важную роль в реализации. [3] FDR2 был разработан факультетом компьютерных наук Оксфордского университета, откуда он был доступен бесплатно.для академического и другого некоммерческого использования. [4]
FDR часто называют средством проверки модели , но технически это средство проверки уточнений , поскольку оно преобразует два выражения процесса CSP в системы помеченных переходов (LTS), а затем определяет, является ли один из процессов уточнением другого в пределах некоторой заданной семантики. модель (следы, сбои, сбои/дивергенции и некоторые другие альтернативы). [5] FDR2 применяет различные алгоритмы сжатия пространства состояний к процессам LTS, чтобы уменьшить размер пространства состояний, которое необходимо исследовать во время уточняющей проверки.
FDR2 выдержал множество выпусков, заменив более ранний инструмент, который в 1995 году теперь назывался FDR1. На смену ему пришел FDR3, полностью переписанная версия, включающая, среди прочего, параллельное выполнение и интегрированную проверку типов. FDR3 выпущен Оксфордским университетом , который также выпустил FDR2 в период 2008-12 годов. [6] ProBE CSP Animator интегрирован в FDR3. Теперь на смену ему пришел FDR4. FDR4 можно приобрести у Cocotec. [7]
Ссылки
[ редактировать ]- ^ Формальные системы (Европа) Ltd.
- ^ Профессор Майкл Голдсмит (теперь также из Оксфордского университета).
- ^ Филиппа Бродфут и Билл Роско. Учебное пособие по FDR и его приложениям . Клаус Хавелунд, Джон Пеникс, Виллем Виссер (редакторы), Проверка модели SPIN и проверка программного обеспечения , Springer-Verlag , Конспекты лекций по информатике , том 1885, стр. 322, 2000.
- ^ Программное обеспечение: FDR2 , коммерческие лицензии можно получить у Formal Systems (Europe) Ltd.
- ^ А. В. Роско (1994). «CSP для проверки модели» . Классический разум: очерки в честь К. А. Хоара . Прентис Холл . п. 353. ИСБН 9780132948449 .
- ^ Введение в FDR3
- ^ Программное обеспечение: FDR4 , коммерческие лицензии можно получить после загрузки и первого запуска.
 | Эта инструментам программирования, статья, посвященная является незавершенной . Вы можете помочь Википедии, расширив ее . |