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.
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.