Chapter 4. Overview of FDR
FDR is a commercial tool [1] designed to establish results about concurrent and reactive systems described in CSP. (In fact, the same underlying ‘engine’ can be applied to a range of other notations that admit similar semantic interpretations; but CSP will suffice for this discussion.)
[1] A product of Formal Systems (Europe) Ltd: visit www.formal.demon.co.uk for details.
With one or two exceptions, [2] FDR obtains its results by comparing two descriptions in a common universe of discourse: a specification and an implementation; in order to determine if the latter is a refinement of the former. If a check is successful, it means that the implementation is a reasonable candidate for substitution into the role of the ...
Get The Modelling and Analysis of Security Protocols: the CSP Approach now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
