Abstract
This chapter describes FDR and how to use this tool effectively. We describe how to interact with the FDR user interface, and how to program in CSP M and its functional sub-language which is roughly equivalent to Haskell. We see what FDR can and cannot do, and how to play to its strengths. For example we see—in an example based on finding a Hamiltonian path—how it is better to code complex systems as parallel compositions rather than as large sequential processes. We show in outline how FDR actually carries out a refinement check, and how this algorithm can be adapted to check determinism. We discuss the relative advantages of depth-first and breadth-first search, and finally show how compression operators that FDR supplies can enable one to (at least partially) overcome the state explosion problem that limits the size of systems the tool can handle.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A broad definition of a ‘model checker’ is any tool which automatically decides whether systems meet their specifications, by somehow exploring all relevant execution paths of the system, and exhibiting a counter-example behaviour if one of the states found does not meet the implied requirements. By a narrower definition, namely that the specification is cast in some, usually temporal, logic such as the one described in Sect. 16.4 and that the role of the tool is to check that the implementation is a model of the specification, FDR is not a model checker.
- 2.
It is likely that the GUI for FDR 3 will look rather different.
- 3.
This is, in fact, the solution to a 16×16 Sudoku puzzle taken from a newspaper. The fact that it has explored only 142 states—as you can see from the Status window—is testament to the great effectiveness of the coding for this sort of puzzle that is set as Exercise 20.2.
- 4.
The reason why this mode is optional at the time of writing is that it is, at present, less sophisticated than one might like. If it is subsequently improved it may well be present by default.
- 5.
P\X is the CSP hiding operator introduced in Chap. 5. It allows all of P’s actions in X to happen, but conceals them from the environment.
- 6.
A process is deterministic (see Sect. 10.5) if it can never either diverge or have the option of performing an event or refusing it.
- 7.
There is a CSP type checker called Checker that, at present, is run independently of other tools like FDR. The reason for this is that the type rules relating to the infix dot “.” as in a.b.c are problematic and can cause a lot of branching, meaning that Checker can take an unreasonably long time and give output that is less than clear. The author hopes that a revised, less generous, type-checker will be created soon, imposing assumptions on this sort of question. Nevertheless Checker can be invaluable, and it was used a great deal by the author in creating the compiler written in CSP described in Chap. 18.
- 8.
See Note 1 at the end of this chapter for a salutary tale of how Quicksort’s use in FDR gave an unexpected result.
- 9.
CSP M is the only functional language known to the author in which sets are supported as first-class objects. They were included because of the importance of sets to CSP as process alphabets, sets to hide, etc. They have proved immensely useful in other contexts also. Probably the reason why they are not seen elsewhere is that they do not fit entirely comfortably with the concept of lazy evaluation: for example to compute the size of a set (as opposed to a list), all its members have to be evaluated completely.
- 10.
In common with Haskell, the implementation of the CSP M language is based on lazy evaluation, which is what allows it to compute with infinite lists. The need to determine which the distinct elements of a set are means that much more evaluation is forced early when using sets as opposed to lists.
- 11.
User-defined data-types that include the process type Proc have only been supported since FDR 2.90.
- 12.
When performing a failures-divergences check, you may also see bracketed counts of the number of implementation states checked for divergence in the manner described on p. 169.
- 13.
This version only allows those c events that are allowed by Spec. See Exercise 8.6 for an alternative version.
- 14.
This is a considerable advance on the situation in 1997 when TPC was written: the unrestricted state space was then well beyond the reach of the workstations on which the author tried this example.
- 15.
Think of running the puzzle backwards from its final state for 15 moves.
- 16.
Although, as we will see, this is true, it does not invalidate solitaire as a benchmark for testing the efficiency of algorithms for searching through an entire state space by BFS or any other strategy.
- 17.
If we wanted the algorithm to respect the ✓-as-signal model of termination we are using in this book, there would be a clause that said that if the node had no τ but a ✓, then the only action it has in the subset is that ✓. However, as remarked on p. 141, FDR does not at present follow that model, so it handles ✓ under the next clause. Replacing P by \(P; {\mathit {SKIP}}\/\) will here, as elsewhere, have FDR treat it as though it were in the ✓-as-signal model.
- 18.
compression09.csp is an extended version of compression.csp, which was one of the example files that accompanied TCP.
- 19.
Bounded model checking means that, instead of searching through a process’s complete state space, one looks only for errors that can be reached within some chosen N steps from the root. It is particularly appropriate for SAT checking because of the algorithms used for the latter, but the CSP notation makes it simple to limit any check in this way.
References
Bird, R.S.: Introduction to Functional Programming Using Haskell, 2nd edn. Prentice Hall, New York (1998)
Een, N., Sorensson, N.: An extensible SAT-solver. In: SAT (2003)
Goldsmith, M.H., Moffat, N., Roscoe, A.W., Whitworth, T., Zakiuddin, M.I.: Watchdog transformations for property-oriented model-checking. In: FME 2003. Springer, Berlin (2003)
Graf, S., Steffen, B.: Compositional minimisation of finite-state systems. In: Proceedings of CAV’90. LNCS, vol. 531. Springer, Berlin (1990)
Hudak, P., Jones, S.L.P., Wadler, P.L., et al.: Report on the programming language Haskell, a non-strict, purely functional language. Sigplan Not. 27, 5 (1992)
Inmos Ltd., occam2 Reference Manual. Prentice Hall, New York (1988)
Jones, G., Goldsmith, M.H.: Programming in occam2. Prentice Hall, New York (1988)
Lazić, R.S.: A semantic study of data-independence with applications to the mechanical verification of concurrent systems. Oxford University D.Phil. Thesis (1997)
Palikareva, H., Ouaknine, J., Roscoe, A.W.: Faster FDR counterexample generation using SAT-solving. In: Proceedings of AVOCS 09 (2009)
Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock. In: Proceedings of the 1st TACAS. LNCS, vol. 1019. Springer, Berlin (1995)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer-Verlag London Limited
About this chapter
Cite this chapter
Roscoe, A.W. (2010). Using FDR. In: Understanding Concurrent Systems. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-1-84882-258-0_8
Download citation
DOI: https://doi.org/10.1007/978-1-84882-258-0_8
Publisher Name: Springer, London
Print ISBN: 978-1-84882-257-3
Online ISBN: 978-1-84882-258-0
eBook Packages: Computer ScienceComputer Science (R0)