2.2 Design and Implementation

B [1] specifications of steam boiler components were defined from the above theories. Standard techniques were used to code up temporal logic constraints. For example the temporal constraint

$$\alpha ~\implies~ (\gamma ~{\cal U}~ \beta)$$

can be formalised by a boolean flag $gamma\_until\_beta$, initialised to FALSE, and preconditions $gamma\_until\_beta = FALSE$ on every controller action except $\gamma$ and $\beta$ and method definitions:

 
   
  gamma_until_beta := TRUE || 
   
  ;
   
  gamma_until_beta := FALSE

A C executable of 3098 lines of code was produced from the B implementations. A number of test scenarios were input to this executable, following the format defined in [2].