Formal Logic Based Heart-Model - Using Event-B for Critical Device Software Systems - page 140

sometimes malfunction. Device related problems have been responsible for a large
number of serious injuries. Many deaths and injuries caused by device failure have
been reported by the FDA [ 28 ], which advocates safety and security guidelines for
using these devices. FDA officials have found that many deaths and injuries related
to the devices are caused by product design and engineering flaws, which can be
considered as firmware problems [ 10 , 17 ].
Providing assurance guarantees for medical devices makes formal approaches
appealing. Formal model based methods have been successful in targeted applica-
tions of medical devices [ 9 , 20 , 21 , 25 , 31 , 32 ]. Over the past decade, there has
been considerable progress in the development of formal methods for improving
confidence in complex software-based systems [ 1 , 13 , 14 ]. Although formal meth-
ods are part of the standard recommendations for developing and certifying medical
systems, the integration of formal methods into the certification process is, in large
part, unclear. In particular, it is a very challenging task to ensure that the end product
of the software-development system behaves securely.
8.1.1 Motivation
The most challenging problem is environment modelling. That is, to validate and to
verify the correct behaviour of a system model requires an interactive formal model
of the environment. For example, a formal model of a cardiac pacemaker or ICD re-
quires a heart model to verify the correctness of the developed system (see Fig. 8.1 ).
No tools and techniques are available to provide environment modelling that would
enable verification of the developed system model. Medical devices are tightly cou-
pled with their biological environment (i.e., the heart) and use actuators and sensors
to interact with the biological environment. Because of this strong relationship be-
tween the medical device (e.g., a pacemaker) and the related biological environment
(i.e., the heart), it is necessary to model the functioning of the medical device within
the biological environment.
The environment model will be independent of the device model, which is helpful
in creating an environment for medical devices that simulates the actual behaviour
of the system. The medical device model will be dependent on the biological en-
vironment. Whenever an undesired state occurs in the biological environment, the
device model must act according to the requirements. The main objective is to use
a formal approach to modelling the medical device and the biological environment
to verify the correctness of the medical system.
To model the biological environment (the heart) for a cardiac pacemaker or ICD,
we propose a method for modelling the heart using logico-mathematical theory [ 33 -
35 ]. The heart model is based on electrocardiography analysis [ 6 , 15 , 24 ], which
models the heart system at the cellular level [ 40 ]. In this investigation, we present a
methodology for modelling a heart that involves extracting a set of biological nodes
(SA node, AV node, etc.), impulse propagation speeds between nodes, impulse prop-
agation times between nodes and cellular automata (CA) for propagating impulses