FDR (software)

FDR ( Failures-Divergences Refinement ) y posteriormente FDR2 , FDR3 y FDR4 son herramientas de software para la verificación de refinamiento , diseñadas para comprobar modelos formales expresados ​​en procesos secuenciales comunicantes (CSP). Las herramientas fueron desarrolladas originalmente por Formal Systems (Europe) Ltd. ^{[ 1 ]} Bill Roscoe , del Departamento de Informática de la Universidad de Oxford, ideó muchos de los algoritmos utilizados por la herramienta y Michael Goldsmith ^{[ 2 ]} fue fundamental en su implementación. ^{[ 3 ]} FDR2 fue desarrollado por el Departamento de Informática de la Universidad de Oxford, desde donde estuvo 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 algún modelo semántico especificado (trazas, fallos, fallos/divergencia 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 tenido muchas versiones, reemplazando a la herramienta anterior ahora conocida como FDR1 en 1995. Fue sucedida por FDR3, una versión completamente reescrita que incorpora, entre otras cosas, ejecución paralela y un verificador de tipos integrado. FDR3 es publicada por la Universidad de Oxford , que también publicó FDR2 en el período 2008-12. ^{[ 6 ]} Un animador ProBE CSP está integrado en FDR3. Ahora ha sido sucedida por FDR4. FDR4 está disponible en Cocotec. ^{[ 7 ]}