1.3.1 Using refinement

A formal system supporting refinement can be used in a number of ways:

• We can develop systems by a series of stepwise refinements, starting with a specification process and gradually refining it into an implementation. Since our notions of refinement are all preserved by the operators of CSP, there is no need to apply refinement rules only at the highest levels in this process. For example, if the parallel composition of P and Q refines a specification S, written

  S PQ

  then we can develop the system further by refining P and Q separately: if PP' and QQ' then the composition of P' and Q' will also refine S:

  S P'Q'

  We do not need to check this condition explicitly.
• The same observation about compositionality, or monotonicity, of refinement, means that it is always possible to replace any component of a system by one that refines it, and retain any correctness properties proved using the same notion of refinement.
• A proposed implementation can be compared to idealised processes representing specifications. These specifications might be complex and be intended to capture the complete behaviour of the implementation, or be simple and capture a single desirable property such as deadlock freedom.
• By proving failures-divergence refinement both ways, two processes can be shown to be equivalent and therefore interchangeable.

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