O'Reilly logo

The Modelling and Analysis of Security Protocols: the CSP Approach by S. A. Schneider, P. Y.A. Ryan

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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’ ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required