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 de comunicación secuencial (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] jugó un papel decisivo en la implementación. [3] FDR2 fue desarrollado por el Departamento de Ciencias de la Computación de la Universidad de Oxford, desde donde estaba disponible gratuitamente para uso académico y otros usos no comerciales. [4]
FDR se describe a menudo 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 alguna semántica especificada. modelo (huellas, fallas, fallas/divergencias y algunas otras alternativas). [5] FDR2 aplica varios algoritmos de compresión del espacio de estados a los LTS de proceso para reducir el tamaño del espacio de estados que debe explorarse durante una verificación de refinamiento.
FDR2 ha pasado por muchos lanzamientos, habiendo reemplazado a la herramienta anterior ahora conocida como FDR1 en 1995. Ha sido sucedido por FDR3, una versión completamente reescrita que incorpora, entre otras cosas, ejecución paralela y un verificador de tipos integrado. FDR3 es lanzado por la Universidad de Oxford , que también lanzó FDR2 en el período 2008-2012. [6] Un animador ProBE CSP está integrado en FDR3. Ahora ha sido sucedido por FDR4. FDR4 está disponible en Cocotec. [7]