The Cardiac Pacemaker - Using Event-B for Critical Device Software Systems - page 172

Chapter 9
The Cardiac Pacemaker
Abstract Building high quality and zero defects medical software-based devices is
a critical task, and formal modelling techniques can effectively help to achieve this
target at the certain level. Formal modelling of a high-confidence medical device,
such as that is too much error prone in operating, is an international Grand Challenge
in the area of Verified Software. Modelling a cardiac pacemaker is one of the pro-
posed challenges, and we consider the complete description of pacemaker's func-
tionalities using an incremental proof-based approach. To assess the effectiveness
of our proposed development methodology and associated techniques and tools, we
select this case study. This chapter presents the development of a cardiac pacemaker
using our proposed development life-cycle methodology from requirement analy-
sis to automatic code generation. In this development, we use formal verification
to verify the correctness of the requirements for a simple and closed-loop model,
model checking to verify the correctness of the system behaviours, real-time ani-
mator to check the system behaviours according to the domain experts (i.e. medical
experts), and finally the code generation tool EB2ALL for generating the codes into
several programming languages. The refinement charts are used to handle the com-
plexity of the system, where it helps to organise the code structure according to the
different operating modes. Formal models are expressed in the Event-B modelling
language, which integrates conditions (called proof obligations) for checking their
internal consistency with respect to the invariants and safety properties. The gener-
ated proof obligations of models are proved by the Rodin tool and desired behaviour
of the system is validated by the ProB tool and real-time animator according to the
medical experts.
9.1 Introduction
Development and production of medical device software and systems are common
crucial issues [ 59 ] for ensuring safe advances in healthcare. The lack of uniform
standard and formalism in the engineering of medical-device software leads many
deficiencies in developing relatively low cost trustworthy software under a limit time
frame. For decades, software failures have cost billions of dollars a year [ 60 ]. During