Formal Development of a Cardiac Pacemaker: From Specification to Code - Formal Methods: Foundations and Applications - page 213

PulseGenerator = PacingPulse ∧ SensingPulse ∧ TimeSt

∧ MeasuredParameters ∧ Leads ∧ Accelerometer

∧ EventMarkers ∧ BatteryStatus ∧ ImplantData

∧ ∧

TelemetrySession ProgrammableParameters

∧

MagnetTest

We model the pacemaker operations as Z operations over PulseGenerator .We
illustrate our approach with the SetTimer operation below, which works as a
counter for the pacemaker, incrementing the time .InZ, Δ St denotes a change to
the state St . We also state that θ ( PulseGenerator \

( time )) , which means that only the time variable is changed; the remaining state
variables are left unchanged.

\ ( time )) = θ ( PulseGenerator

SetTimer
Δ PulseGenerator

time = time +1
θ ( PulseGenerator \

( time )) = θ ( PulseGenerator

\

( time ))

According to its requirements [13], the pacemaker must be capable of sens-
ing pulses from the heart by using leads connected to the heart's chambers.
There are three relevant moments during pulse measurement. As illustrated in
Figure 2, the pacemaker must register the pulse start time, the maximal ampli-
tude of the pulse and the moment when the pulse ends .

Fig. 2. Relevant moments during pulse measurement

As an example, we present the VentricleStartTime operation [7] that reg-
isters the initial moment of a sensed pulse in the ventricle chamber. Its pre-
condition states that: (1) the current bradycardia operation mode must sense
either the ventricle chamber or both chambers ( bo mode . chambers sensed

∈

{ ); (2) there was no previously sensed pulse in the

ventricle ( r wave = 0); and (3) the measured pulse amplitude from ventricle
chamber is higher than the actual pulse ( v curr measurement > r wave ). If
these preconditions are satisfied, the pacemaker will update the value of r wave

C VENTRICLE , C DUAL }