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

to construct a pacemaker system without any previous knowledge on basic car-
diological information such as pacing modes , timing cycles ,and event markers .
Researchers that intend to embrace the challenge need a large amount of ad-
ditional resources such as pacemaker guides [22] and topics in the cardiology
domain [7]. As a consequence of the lack of a detailed specification of some com-
ponents originally presented in [13] due to commercial reasons, a small number
of functionalities of the pacemaker have not yet been modelled. For instance, we
have no specific information about the internal operations of the rate-adaptive
algorithm , which is used by the pacemaker to recognise the level of body's move-
ment and increase the frequency of pulses delivered. Besides time ,wewerenot
able to specify other non-functional requirements due to the lack of specification
in the original document.
There are other research groups that also have undertaken the pacemaker
case study. An informal one-day meeting was held in November 2009, during
the Second World Congress on Formal Methods in Eindhoven. Research groups
involved with the pacemaker case study, including researchers from Boston Sci-
entific, were present in this meeting. On this occasion, the research groups could
present their most recent results on the pacemaker challenge and compare their
work. Moreover, we could discuss some issues related to the challenge, such as
the lack of a detailed specification of some operations of the pacemaker, as dis-
cussed in this paper, and also the availability of possible test scenarios to be
used in order to validate the pacemaker system. Despite the widespread interest
in the challenge, few results have been published.
An approach using VDM was used by Macedo et. al in [14], where they
constructed a model based on a subset of the functionalities of the pacemaker
in VDM. They modelled 8 of the 19 bradycardia operation modes including the
corresponding programmable parameters and developed not only a sequential
model of the system, but also a concurrent and a distributed real-time model
of the pacemaker using VDM++. They constructed several test cases in order
to validate their sequential model, and re-used some of these to validate their
concurrent and also their distributed real-time model.
Event-B [15] has been used by researchers from INRIA to undertake the pace-
maker case study. This work suggests an incremental approach in which new
functionalities of the system are added to the model at each refinement step.
They validate their system using ProB with many test scenarios like absence of
intrinsic pulses from the heart and rate-adaptive pacing modes .
Finally, in [24], Tuan et. al proposed a formal model of the pacemaker based on
its behaviour including the communication with the external environment. They
created a real-time model of the pacemaker using timed extensions of CSP [20]
and used the model checker Process Analysis Toolkit (PAT) [23] in order to verify
critical properties, such as deadlock freeness and heart rate limits .
In a near future, we will investigate approaches to generate hardware proto-
types from our Perfect Developer code. Furthermore, we also intend to specify
the missing parts of the specification as soon as we receive a more detailed
information regarding those features, from Boston Scientific and the Software