1.1 What is FDR?

FDR (Failures-Divergence Refinement) is a model-checking tool for state machines, with foundations in the theory of concurrency based around CSP--Hoare's Communicating Sequential Processes [Hoare85]. Its method of establishing whether a property holds is to test for the refinement of a transition system capturing the property by the candidate machine. There is also the ability to check determinism of a state machine, and this is used primarily for checking security properties [Roscoe95], [RosWood94]. The main ideas behind FDR are presented in [Roscoe94].

Previous versions of the tool (up to 1.4x) used only explicit model-checking techniques: the check proceeds by a recursion induction which fully expands the reachable state-space of the two systems and visits each pair of supposedly corresponding states in turn. Although it is very efficient in doing this and can deal with processes with approximately 10⁷ [10 to the power 7] states in a few hours on a typical workstation, the exponential growth of state-space with the number of parallel processes in a network represents a significant limit on its utility.

The primary aim in the development of the new version of the tool, FDR2, was to improve on the flexibility and scalability of the tool. In particular, FDR2 offers

• support for operators outside the core CSP and, indeed, completely different languages
• improved handling of multi-way synchronisation, with the representation of firing rules based on the events which components may engage in, rather than pattern-matching on their states
• relaxation of some of the restrictions on the CSP scripts, in particular the strict distinction between "high-level" (parallel or hiding) and "low-level" (parametrised or recursive) constructs
• provision of a much more powerful language for data types and expressions
• potential for "lazy" exploration of systems (allowing some non-finite-state specifications, such as "is a buffer")
• the ability to build up a system gradually, at each stage compressing the subsystems to produce an equivalent process with (hopefully) many less states.

This last item means that FDR2 can check systems which are sometimes exponentially larger than those which FDR1 can--such as a network of 10²⁰ [10 to the power 20] (or 100¹⁰⁰ [100 to the power 100]) dining philosophers [RosEtAl95].

The "back-end" state-exploring code has been completely re-crafted. FDR2 marries this to a new parser/compiler based on Scattergood's implementation of the operational semantics of CSP [Scat95]. Experimental hooks for attaching "alien" state-machine descriptions have been developed, so it is possible for FDR2 to operate on files created by other techniques.

Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.