5.1.2 Compressions in context

FDR2 will take a complex CSP description and build it up in stages, compressing the resulting process each time. Ultimately we expect these decisions to be at least partly automated, but in current versions almost all compression directives must be included in the syntax of the process in question. At present, the only automatic applications of these techniques are:

• Bisimulation of all "low-level" leaf processes (by construction).
• Normalisation of the left hand side of a check.

One of the most interesting and challenging things when incorporating these ideas is preserving the debugging functionality of the system. The debugging process becomes hierarchical: at the top level we will find erroneous behaviours of compressed parts of the system; we will then have to debug the pre-compressed forms for the appropriate behaviour, and so on down. On very large systems (such as that discussed in the next section) it will not be practical to complete this process for all parts of the system. Therefore the debugging facility initially works out subsystem behaviours down no further than the highest level compressed processes, and only investigates more deeply when directed by the user (as described in 2.9 The FDR2 Process Debugger and 3.2.3 Debugging).

The way a system is composed together can have an enormous influence on the effectiveness of hierarchical compression. The following principles should generally be followed:

1. Put processes which communicate with each other together early. For example, in the dining philosophers, you should build up the system out of consecutive fork/philosopher pairs rather than putting the philosophers all together, the forks all together and then putting these two processes together at the highest level.
2. Hide all events at as low a level as is possible. The laws of CSP allow the movement of hiding inside and outside a parallel operator as long as its synchronisations are not interfered with. In general therefore, any event that is to be hidden should be hidden the first time (in building up the process) that it no longer has to be synchronised at a higher level. The reason for this is that the compression techniques all tend to work much more effectively on systems with many -actions.
3. Hide all events that are irrelevant to the specification you are trying to prove.

Hiding can introduce divergence, and therefore invalidate many failures/divergences model specifications. However, in the traces model it does not alter the sequence of unhidden events, and in the stable failures model does not alter refusals which contain every hidden event. Therefore if you are only trying to prove a property in one of these models -- or if it has already been established by whatever method that the system is divergence free -- the improved compression we get by hiding extra events makes it worthwhile doing so.

Two examples of this, one based on the COPY chain example we saw above and one on the dining philosophers are discussed in more detail in [RosEtAl95]. The first is probably typical of the gains we can make with compression and hiding; the second is atypically good.

• Hiding and safety properties
• Hiding and deadlock

Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.