Introduction¶

FDR is a tool for analysing programs written in Hoare’s CSP notation, in particular machine-readable CSP namely CSPM, which combines the operators of CSP with a functional programming language. The original FDR was written in 1991 by Formal Systems (Europe) Ltd, and a completely revised version FDR2 was released in the mid-1990s by the same organisation. The current version of the tool is FDR4, first released in October 2016 following FDR3 which was first released in 2013. Both of these versions were released by the University of Oxford, which also released FDR2 versions 2.90 and above in the period 2008-12.

FDR4.0 has extremely similar functionality to FDR2.94, but is completely re-written. The main differences are:

1. The user interface has been completely revised.
2. The debugger has been completely revised and gives simultaneous information about all components of a system, rather than one at a time.
3. There is an integrated type checker for CSP_M.
4. It now uses multi-core parallelism to speed up its operation.
5. A version of the ProBE CSP animator has been integrated.
6. There is a utility for drawing graphical representations of the labelled transition systems that represent processes within FDR.

The only significant functionality of FDR2.94 that FDR4.0 lacks is support for the revivals and refusal testing models of CSP and their divergence-strict versions (i.e. [V=, [VD=, [R= and [RD=). Note that the batch mode of FDR2.94 has been replaced by a new machine-readable interface based on standard formats (JSON, XML and YAML are supported).

FDR uses many algorithms and data structures. The ones used in FDR4 are in some cases the same, in some cases mildly modified, and in other cases completely new. Papers about FDR4 and its development can be found in References. Many books and papers have been written about CSP and earlier versions of FDR.

@inproceedings{fdr,
   title={{FDR3 --- A Modern Refinement Checker for CSP}},
   author={Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov, A.W. Roscoe},
   booktitle={Tools and Algorithms for the Construction and Analysis of Systems},
   year = {2014},
   pages = {187-201},
   volume={8413},
   series={Lecture Notes in Computer Science},
   editor={Ábrahám, Erika and Havelund, Klaus},
}

@manual{fdrmanual,
   title={{Failures Divergences Refinement (FDR) Version 3}},
   author={Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov, A.W. Roscoe},
   year={2013},
   url={https://www.cs.ox.ac.uk/projects/fdr/},
}