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

the heart within an interval programmed by the cardiologist regardless of any
electrical activity in the heart.
In the next section we present our formalisation of the pacemaker using Z.

3 Pacemaker in Z

Our formal specification of the pacemaker is based on an informal specifica-
tion [13] of an old Boston Scientific's pacemaker model [5]. We decided to de-
velop a model of the pacemaker, hereafter referred to as pulse generator ,asa
modularised Z state PulseGenerator making strong use of the Z schema cal-
culus. It allows us to model each component of the pacemaker separately. The
components of the PulseGenerator state are modelled as Z schemas with their
variables and state invariants. The PulseGenerator [9] modularisation, as ex-
pected, helped us to keep the Z model comprehensible while moving into Perfect
Developer. Furthermore, our specification also helped us in the development of
a graphical user interface in C# because in the object oriented generated code
each Z component was refined to a C# class, making it easier to access variables
and methods from the PulseGenerator class.
Our PulseGenerator state is composed by a number of components like the
set of programmable parameters, the set of measured parameters, the battery
status component, and time. There are also many other components of the
PulseGenerator state that are not presented here for the sake of conciseness 1 .As
an example, we briefly present the time state component, called TimeSt ,which
is responsible for storing all the information regarding time. It acts as a time
counter and also stores information regarding the last occurrences of pulses from
the heart, measured by the pacemaker.

TimeSt
time :

N
a start time , v start time , a max , v max :

N
a delay , v delay , a curr measurement , v curr measurement :

N

In our convention, variables related to the atrial chamber are prefixed with a
and, similarly, variables related to the ventricular chamber are prefixed with v .
Hence, the variable a start time stores the initial moment of a pulse detected
in the atrium, a max stores the maximum value of the pulse and a delay stores
the value of the duration of the pulse in the atrium chamber. The measurement
of pulses coming from atrial and ventricle are defined as a curr measurement
and v curr measurement , respectively.
The other components of the PulseGenerator state are modelled in a sim-
ilar fashion. In some cases, however, state invariants are required for restrict-
ing the state components according to the informal specification. Finally, the
PulseGenerator state is modelled as the conjunction of each component.

1 The

pacemaker full specification can be downloaded from

http://sites.google.com/site/pacemakerinz/pacemaker-in-z.pdf