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

with the value of v curr measurement and register ( v start time = time )the
initial time of that pulse.

VentricleStartTime
Δ PulseGenerator

bo mode . chambers sensed

∈{

C VENTRICLE , C DUAL

}

v curr measurement > r wave

∧

r wave =0

r wave = v curr measurement

∧

v start time = time

( r wave , v start time ))
= θ ( PulseGenerator

θ ( PulseGenerator \

\ ( r wave , v start time ))

We modelled the detection of pulses in the heart as distinct Z operations. As
presented above, VentricleStartTime registers the initial moment of sensed pulse
in the ventricle. A second operation, VentricleMax , is responsible for storing
the maximal pulse amplitude. Finally, VentricleEnd registers the moment when
the pulse ends. We also modelled the operation VentricularMeasurement as the
disjunction of each of these operations as illustrated below. In a similar way, we
modelled operations for the atrial chamber, which can be found in [8].

VentricularMeasurement = VentricleStart ∨ VentricleMax ∨ VentricleEnd

The Z operation SensingModule , defined below, is responsible for the mea-
surement of pulses coming from the heart. This operation is the disjunction
of the VentricularMeasurement operation, presented above, and the operation
AtrialMeasurement modelled similarly.

SensingModule = VentricularMeasurement ∨ AtrialMeasurement

The main purpose of the pacemaker is to supply the heart needs by delivering
a therapy defined by the cardiologist. We specified the operation BradyTherapy
( bradycardia therapy ) as the sequential composition of four operations given be-
low. The first one is the SetTimer presented above: the pacemaker increments its
timer. Next, the operation SensingModule , as presented above, registers the exact
moment of the pulses in the heart. Then, the pacemaker records the markers from
sensed events, by invoking the operation SensingMarkers . Finally, SetMode ( set
the bradycardia operation mode ), responds to the heart needs, based on the pro-
grammable parameters values defined by the cardiologist, and delivering pulses
if necessary.

BradTherapy = SetTimer 9 SensingModule 9 SensingMarkers 9 SetMode

In [9], we discussed some of the verification made on this formal specification
using the theorem prover ProofPower-Z. This verification included validating the
system initialisation and its consistency regarding the state invariant. The next
step, which is the subject of this paper, is to get a verified code of the pacemaker
suitable to be executed. In the next section, we discuss some of the possibilities
for moving from our Z specification into executable code.