4.1. Comparing processes
The relationships between processes that FDR calculates are denotational properties: what is of interest is a comparison of their observable behaviours (in particular, for refinement, that every observation possible of the implementation should also be possibly observed of the specification), not the internal evolution that gives rise to them. What constitutes an observable behaviour depends on the kind of property one is interested in:
Traces, the finite sequences of visible events a process may engage in, give the coarsest useful comparison; refinement in the traces model corresponds to language inclusion in automata theory, and to Hennessy’s ‘may’ testing [40]. Assuming that the specification describes what is ‘good’ ...
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.
