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

Formal Development of a Cardiac Pacemaker:
From Specification to Code

Artur O. Gomes and Marcel V.M. Oliveira

Universidade Federal do Rio Grande do Norte, Brazil
[e-mail], [e-mail]

Abstract. This paper presents a formal development of a cardiac pacing
system based on a Boston Scientific 's model, a pilot case study from the
Grand Challenge in Software Verification . We present a summary of our
Z model of the system, its translation into Perfect Developer, and the
code generation and execution. Further practical result and analysis are
also in the context of this paper.

Keywords:

formal modelling, Z, refinement, Perfect Developer, pacemaker.

1 Introduction

The cardiac pacemaker [5], whose specification document was made available
by the Software Quality Research Laboratory [1], at McMaster University in
Canada, was proposed as one of the pilot case studies of the Grand Chal-
lenges in Software Verification [11], maintained by the Verified Software Ini-
tiative (VSI) [12]. The main objective of this project is to use formal methods
throughout the development process of real case studies, stimulating researchers
with experience in formal methods to apply their knowledge in a set of pilot
case studies, like the pacemaker, showing empirically that formal methods have
reached an acceptable level of usability even in industrial scale applications.
The pacemaker is relevant since it is a very good example of a critical system
which needs to have strong guarantees that the system will work according to
its requirements. Any failure or bug may cause serious damages to patients.
In [9], we use the Z language [25] to formally specify the pacemaker. More-
over, we discuss how we used the theorem prover ProofPower-Z [17] to prove
theorems that validate the consistency of the system. In this paper, we present
our last results in the pacemaker case study by providing a means to execute the
model: we present a translation of our Z model [9] into Perfect Developer [2].
Using this tool, we are able to verify the translated code by using its internal
theorem prover fully automatically and refining the verified specification into
programming languages like Java, C#, C++ or ADA.
Section 2 gives an overview of the pacemaker system. We will briefly present
our model of the system using Z in Section 3. Then, we discuss some options
that were considered to move into a verified code of the pacemaker in Section 4.
In Section 5, we present some fragments of the translation of the pacemaker