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

Fig. 9.11 Real-time animation of cardiac pacemaker

We have done this experiment in off-line mode, means we have used our architec-
ture to test the real-time data set of ECG signal that is already collected. ECG signal
collection and features extraction in on-line mode is too expensive due to complex
data-acquisition process and limitation of feature extracting algorithms. So, we have
used the ECG signal and feature extraction algorithms for our experiment from the
MIT-BIH Database Distribution [ 54 ].
We have downloaded the ECG signal from ECG data bank [ 54 ]. The ECG sig-
nals are freely available for academic experiments. We have applied some algo-
rithms to extract the features (P, QRS, PR, etc.) from the ECG signal and stored it
into a database. We have written down some Macromedia Flash scripts to interface
between Flash tool and Brama component, to pass the real data set as a param-
eter from a database to the Event-B model. No any tool is available to interface
between database and the Event-B model. Extra Macromedia Flash script coding
and the Brama animation tool help to test the Event-B formal model of the car-
diac pacemaker on the real-time data set. We have designed an animated graphic of
heart and pacemaker in Macromedia Flash, where this animated model represents
the pacing activity in the right ventricular chamber. This animated model simulates
the behaviour of heart according to the bradycardia operating modes and animates
the graphic model. The animation of the model is fully based on the Event-B model.
Event-B model is executing all events according to the parametric value. These para-
metric values are the extracted features from the ECG signal, which are passing into
the Event-B model.
Figure 9.11 represents an implementation of proposed architecture on the for-
mal model of a cardiac pacemaker case study. According to the architecture, data
acquisition unit collects the ECG signal and features extractions are done by the
feature extraction or parameter estimation unit. The extracting features are stored in
the database XML file format. Macromedia Flash tool helps to design the animated
graphics of the heart and pacemaker. Brama plug-in helps to communicate between
animated graphics and Event-B formal model of the single electrode cardiac pace-
maker. Finally, we have tested a real-time data set in the formal models without
generating the source code.