FDR (Failures-Divergences Refinement) and subsequently FDR2, FDR3 and FDR4 are

refinement Refinement may refer to: Mathematics * Equilibrium refinement, the identification of actualized equilibria in game theory * Refinement of an equivalence relation, in mathematics ** Refinement (topology), the refinement of an open cover in mathem ...

checking

software tool A programming tool or software development tool is a computer program that software developers use to create, debug, maintain, or otherwise support other programs and applications. The term usually refers to relatively simple programs, that can b ...

s, designed to check

formal model In logic, mathematics, computer science, and linguistics, a formal language consists of string (computer science), words whose symbol (formal), letters are taken from an alphabet (formal languages), alphabet and are well-formedness, well-formed ...

s expressed in

Communicating sequential processes In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or pro ...

(CSP). The tools were originally developed by Formal Systems (Europe) Ltd.

Bill Roscoe Andrew William Roscoe is a Scottish computer scientist. He was Head of the Department of Computer Science, University of Oxford from 2003 to 2014, and is a Professor of Computer Science. He is also a Fellow of University College, Oxford. Educ ...

of the

Department of Computer Science, University of Oxford The Department of Computer Science is the computer science department of the University of Oxford, England, which is part of the university's Mathematical, Physical and Life Sciences Division. It was founded in 1957 as the Computing Laboratory. ...

devised many of the algorithms used by the tool and

Michael Goldsmith Michael Goldsmith (March 6, 1951—November 1, 2009) was a law professor at Brigham Young University's J. Reuben Clark Law School. Early life and education Michael Goldsmith was born March 6, 1951 in Tel Aviv, Israel and immigrated to the Uni ...

was instrumental in the implementation. FDR2 was developed by

from where it was freely available for academic and other non-commercial use. FDR is often described as a

model checker In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software system ...

, but is technically a ''

'' checker, in that it converts two CSP process expressions into

Labelled Transition System In theoretical computer science, a transition system is a concept used in the study of computation. It is used to describe the potential behavior of discrete systems. It consists of state (computer science), states and transitions between states, ...

s (LTSs), and then determines whether one of the processes is a refinement of the other within some specified

semantic model A conceptual model is a representation of a system. It consists of concepts used to help people know, understand, or simulate a subject the model represents. In contrast, physical models are physical object such as a toy model that may be assembl ...

(traces, failures, failures/divergence and some other alternatives). FDR2 applies various

state-space A state space is the set of all possible configurations of a system. It is a useful abstraction for reasoning about the behavior of a given system and is widely used in the fields of artificial intelligence and game theory. For instance, the toy ...

compression algorithms to the process LTSs in order to reduce the size of the state-space that must be explored during a refinement check. FDR2 has gone through many releases, having replaced the earlier tool now referred to as FDR1 in 1995. It has been succeeded by FDR3, a completely re-written version incorporating amongst other things parallel execution and an integrated type checker. FDR3 is released by the

University of Oxford , mottoeng = The Lord is my light , established = , endowment = £6.1 billion (including colleges) (2019) , budget = £2.145 billion (2019–20) , chancellor ...

, which also released FDR2 in the period 2008-12. A ProBE CSP Animator is integrated in FDR3. It now has been succeeded by FDR4. FDR4 is available from Cocotec.Software: FDR4
with commercial licences obtainable after download and first start

References

Model checkers Concurrent computing Oxford University Computing Laboratory {{programming-software-stub