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 интегрирован в FDR3. Теперь его сменил FDR4. FDR4 доступен от Cocotec. [7]