Biomedical Engineering Reference
In-Depth Information
Ta b l e 8 . 3
Proof statistics
Model
Total number of POs
Automatic proof
Interactive proof
Abstract model
29
22 (76 %)
7 (24 %)
First refinement
9
6 (67 %)
3 (33 %)
Second refinement
159
155 (97 %)
4 (3 %)
Third refinement
10
1 (10 %)
9 (90 %)
Fourth refinement
11
10 (91 %)
1 (9 %)
Total
218
194 (89 %)
24 (11 %)
8.5.7 Model Validation and Analysis
There are two main validation activities in Event-B, and both are complementary
for designing a consistent system in the medical domain;
consistency checking
and
model analysis
. This section validates the model by using ProB tool [
26
] and proof
statistics. “Validation” refers to the activity of gaining confidence that the devel-
oped formal models are consistent with the requirements. We have used the ProB
tool that supports
automated consistency checking
of Event-B machines via model
checking [
11
] and constraint-based checking [
18
]. This tool assists us to validate
the heart model according to the conduction network and a set of landmark nodes.
It is the complementary use of both techniques to develop formal models of critical
systems, where high safety and security are required. The heart model is carefully
verified through animations and under supervision of physiologist and cardiologist.
We have validated various scenario cases of normal and abnormal heart conditions,
and we have also tested morphological behaviour [
3
,
6
] of the ECG during impulse
propagation from the SA node (A) to the Purkinje fibres (F, H) in the ventricles. The
logic-based mathematical model of the heart can generate all possible scenarios of
normal and abnormal heart conditions in the ECG caused by changes in time and
velocity among landmark nodes. ProB was very useful in animating all models and
in verifying the absence of error (no counter-examples exist) and deadlock.
Table
8.3
expresses the proof statistics of the development using the Rodin tool.
These statistics measure the size of the model, the proof obligations generated and
discharged by the Rodin prover and those are interactively proved. The complete
development of the heart model results in 218 (100 %) proof obligations, within
which 194 (89 %) are proved automatically by the Rodin tool. The remaining 24
(11 %) proof obligations are proved interactively using Rodin tool. For the heart
model, many proof obligations are generated because of the introduction of the new
functional behaviours. To guarantee the correctness of these functional behaviours,
we have established various invariants in the incremental refinements. Most of the
proofs are interactively discharged in the third refinement of the heart model. These
proofs are quite simple, and have been discharged with the help of simplifying pred-
icates. Few proof obligations are proved interactively in other refinements. The in-
cremental refinement of the heart system helps to achieve a high degree of automatic
proof.
Search WWH ::
Custom Search