Refinement Chart - Using Event-B for Critical Device Software Systems - page 99

Fig. 6.3 Refinements of one-electrode pacemaker using the refinement chart

a code designer to improve the code structures, code optimisation, and code genera-
tion techniques. Every incremental refinement represents additional functionalities.
This refinement-based structure may greatly improve the safety, hardware integra-
tion and guidelines to develop the critical systems. We, therefore, propose a simple
methodology of system integration using the refinement chart, that seeks to min-
imise the effort and overhead.

6.4 Applications and Case Studies

We have applied the refinement chart [ 11 ] in the system development of a cardiac
pacemaker for handling the complexity of the system model (see Chap. 9 ). Refine-
ment chart helps to model the system integration, which also complies with refine-
ment based formal development. The block diagrams of the refinement chart help to
build the complete system and used to handle the complexity of the whole system
through decomposing in multiple independent parts. Here, refinement chart models