4.1 Building a Model

When approaching a new problem with FDR, it is tempting to dump a detailed description of the problem into CSP as quickly as possible and “see how well FDR copes.” The results of such an exercise are frequently disappointing. The model produced is usually intractable, and ad-hoc attempts to simplify it tend to reduce its coherence and destroy any confidence in its accuracy. Much better results are achieved by starting from a minimal model and incrementally adding and testing features; in particular, incremental testing will reveal flaws soon after their addition to the model.

Note that even if the initial model is small, the choice of identifiers and careful commenting is still important. In particular, single character process and tag names are likely to cause readability problems.

4.1.1 Abstract model

When adding detail to a simple model, it is only necessary to add those details which are necessary to support the tests you intend to make. For example, the correctness of many communication protocols is independent of the precise values being communicated and it may suffice to replace the actual (large) space of values with a space of one or two values. (Although such a simplification has intuitive appeal, the theory underlying it is still an active research area.)

As well as simplifying the values communicated, it may be possible to omit some events entirely and eliminate state from component processes. For example, the CSP vending machine of [Hoare85] is given by

VM = coin -> choc -> VM

This discards almost all details including various coin sizes, the need to provide change and the possibility that the machine may need refilling. Such abstraction may introduce non-determinism, for example if we consider that the machine may become empty without modelling the level, we obtain

VME = coin -> (VME |~| choc -> VME)

Nevertheless, such an abstraction can be useful. If we can show that VME satisifies some specification then the same will be true for a more detailed model which does model the level, such as

VML(n) = coin -> (if n>0 then choc->VML(n-1) else VML(0))

since

VME [= VML(N)

In extreme cases it may suffice to model a component with interface A as CHAOS(A), the most non-deterministic divergence-free process with that interface.

4.1.2 Use components

For sound engineering reasons, complex systems are built out of simpler components with the correctness of the system as a whole dependent on properties of the components, rather than on precise implementation details. For properly designed systems, this structure can be exploited to reduce the work involved in checking the system. For example, suppose we can write

SYSTEM = F(C_1, C_2)

for some components C_1 and C_2, and that we wish to check that

SPEC [= SYSTEM

and that the properties of the subcomponents can be expressed as S_1 and S_2. Then we can establish the result we require by three simpler tests, namely

S_1 [= C_1

S_2 [= C_2

SPEC [= F(S_1, S_2)

since

SPEC [= F(S_1, S_2) [= F(C_1, C_2) = SYSTEM

follows by the compositional nature of the CSP operators.

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.