Worldlex Wiki FDR ( Failures-Divergences Refinement ), puis FDR2 , FDR3 et FDR4, sont des outils logiciels de vérification de raffinement , conçus pour contrôler les modèles formels exprimés sous forme de processus séquentiels communicants (CSP). Ces outils ont été initialement développés par Formal Systems (Europe) Ltd. Bill Roscoe , du département d'informatique de l'université d'Oxford, a conçu de nombreux algorithmes utilisés par l'outil, et Michael Goldsmith a joué un rôle déterminant dans son implémentation. FDR2 a été développé par le département d'informatique de l'université d'Oxford, qui le mettait à disposition gratuitement pour un usage académique et non commercial.
FDR est souvent décrit comme un vérificateur de modèles , mais il s'agit techniquement d'un vérificateur de raffinements . En effet, il convertit deux expressions de processus CSP en systèmes de transition étiquetés (LTS), puis détermine si l'un des processus raffine l'autre selon un modèle sémantique spécifié (traces, échecs, échecs/divergence et autres alternatives). FDR2 applique divers algorithmes de compression d'espace d'états aux LTS des processus afin de réduire la taille de l'espace d'états à explorer lors d'une vérification de raffinement.
FDR2 a connu de nombreuses versions, ayant remplacé l'outil précédent, désormais appelé FDR1, en 1995. Il a été remplacé par FDR3, une version entièrement réécrite intégrant notamment l'exécution parallèle et un vérificateur de types. FDR3 est distribué par l' Université d'Oxford , qui avait également distribué FDR2 entre 2008 et 2012. Un module d'animation ProBE CSP est intégré à FDR3. Ce dernier a depuis été remplacé par FDR4, disponible auprès de Cocotec.