FDR ( Refinamiento de fallas-divergencias ) y posteriormente FDR2 , FDR3 y FDR4 son herramientas de software de verificación de refinamiento , diseñadas para verificar modelos formales expresados en procesos secuenciales de comunicación (CSP). Las herramientas fueron desarrolladas originalmente por Formal Systems (Europe) Ltd. [1] Bill Roscoe del Departamento de Ciencias de la Computación de la Universidad de Oxford ideó muchos de los algoritmos utilizados por la herramienta y Michael Goldsmith [2] fue fundamental en la implementación. [3] FDR2 fue desarrollado por Departamento de Ciencias de la Computación, Universidad de Oxford, desde donde estaba disponible gratuitamente para uso académico y otros usos no comerciales. [4]
FDR a menudo se describe como un verificador de modelos , pero técnicamente es un verificador de refinamiento , ya que convierte dos expresiones de proceso CSP en sistemas de transición etiquetados (LTS) y luego determina si uno de los procesos es un refinamiento del otro dentro de una semántica específica. modelo (rastros, fallas, fallas/divergencia y algunas otras alternativas). [5] FDR2 aplica varios algoritmos de compresión de espacio de estado a los LTS de proceso para reducir el tamaño del espacio de estado que debe explorarse durante una verificación de refinamiento.
FDR2 ha pasado por muchos lanzamientos, reemplazando la herramienta anterior ahora conocida como FDR1 en 1995. Ha sido reemplazada por FDR3, una versión completamente reescrita que incorpora, entre otras cosas, ejecución paralela y un verificador de tipo integrado. FDR3 es publicado por la Universidad de Oxford , que también lanzó FDR2 en el período 2008-12. [6] Un ProBE CSP Animator está integrado en FDR3. Ahora ha sido sucedido por FDR4. FDR4 está disponible en Cocotec. [7]