Abstract
FDR [1] is a refinement checker for the process algebra CSP [2,4], based on that language’s well-established semantic models. FDR stands for Failures-Divergences Refinement, after the premier model. In common with many other model checkers, it works by “determinising” (or normalising) a specification and enumerating states in the cartesian product of this and the implementation. Unlike most, the specification and implementation are written in the same language. Under development by its creators, Formal Systems (a spin-off of the Computing Laboratory) since 1991, it now offers a range of state compression methods. On current workstations it can work at up to 20M states/hour with only a small degradation on moving to disc-based storage.
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
References
Formal Systems. FDR web site: http://www.formal.demon.co.uk/FDR2.html
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Lowe, G.: Casper web site: http://www.mcs.le.ac.uk/~gl7/Security/Casper/
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Broadfoot, P., Roscoe, B. (2000). Tutorial on FDR and Its Applications. In: Havelund, K., Penix, J., Visser, W. (eds) SPIN Model Checking and Software Verification. SPIN 2000. Lecture Notes in Computer Science, vol 1885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722468_18
Download citation
DOI: https://doi.org/10.1007/10722468_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41030-0
Online ISBN: 978-3-540-45297-3
eBook Packages: Springer Book Archive