The Cardiac Pacemaker - Using Event-B for Critical Device Software Systems - page 180

Fig. 9.4 Refinement structure of bradycardia operating modes of the pacemaker

gorithm case studies [ 9 , 55 ]. This time pattern is fully based on a timed automaton.
The timed automaton is a finite state machine that is useful to model the components
of real-time systems. In a model, timed automata interacts with each other and de-
fines a timed transition system. Besides ordinary action transitions that can represent
input, output and internal actions. A timed transition system has time progress tran-
sitions. Such time progress transitions result in synchronous progress of all clock
variables in the model. Here, we apply the time pattern in modelling to synchro-
nise the sensing and pacing stimulus functions of the pacemaker system in con-
tinuous progressive time constraint. In the model, events are controlled under time
constraints, which means action of any event activates only when time constraint
satisfies on a specific time. The time progress is also an event, so there is no modifi-
cation of the underlying Event-B language. It is only a modelling technique instead
of a specialised formal system. The timed variable is in

( natural numbers ), but
time constraint can be written in terms involving unknown constants or expressions
between different times. Finally, the timed event observations can be constrained by
other events, which determine future activations.

N

9.4 Refinement Structure of a Cardiac Pacemaker

We present a block diagram (see Fig. 9.4 ) of a hierarchical tree structure of the pos-
sible bradycardia operating modes for a pacemaker. The hierarchical tree structure
depicts a stepwise refinement from abstract to concrete models of the formal de-
velopment for a pacemaker. Each level of refinement introduces new features of a
pacemaker as functional and parametric requirements.
The root node indicates a cardiac pacemaker system. The next two branches show
two classes of pacemaker: one-electrode pacemaker and two-electrode pacemaker.
The one-electrode pacemaker branch is divided into two parts to indicate different