Formalisation of Electrocardiogram (ECG) - Using Event-B for Critical Device Software Systems - page 290

Table 10.3 Proof statistics

Model Total number of POs Automatic proof Interactive proof

Abstract model 41 33 (80 %) 8 (20 %)

First refinement 61 54 (88 %) 7 (12 %)

Second refinement 41 38 (92 %) 3 (8 %)

Third refinement 51 36 (70 %) 15 (30 %)

Fourth refinement 60 35 (58 %) 25 (42 %)

Fifth refinement 43 22 (51 %) 21 (49 %)

Sixth refinement 38 14 (36 %) 24 (64 %)

Seventh refinement 124 29 (23 %) 95 (77 %)

Eighth refinement 52 30 (57 %) 22 (43 %)

Ninth refinement 21 9 (42 %) 12 (52 %)

Tenth refinement 67 43 (64 %) 24 (36 %)

Total 599 343 (58 %) 256 (42 %)

ing refinement approach. In the table, the POs column represents the total number of
proof obligations generated for each level. The interactive POs column represents
the number of those proof obligations that have to be proved interactively. Those
proof obligations that are not proved interactively are proved completely automati-
cally by the prover. The complete development of the ECG interpretation protocol
system results in 599 (100 %) proof obligations, in which 343 (58 %) are proved
automatically by the Rodin tool. The remaining 256 (42 %) proof obligations are
proved interactively using Rodin tool. In seventh refinement, numbers of POs are
higher than other refinements because significantly in this level; number of vari-
ables and events are higher than another level of refinements. All the proofs are
discharged completely automatic as well as interactive for all refinement levels. All
these proofs are involved either by the complexity of the formal expression that
proved by do case or finiteness constraints on a set of leads. The main interactive
steps involved instantiating for total function of the different features of the ECG
interpretation in every level of refinement. In order to guarantee the correctness of
the system, we have established various invariants in the stepwise refinement. All
these invariants are derived from the original protocol to verify the correctness and
consistency of the system under the guidance of the cardiologist expert. Most of
the invariants are introduced for checking the abnormality of the features of the
ECG signal. Detection of an abnormal criteria, the heart shows surety of a particu-
lar disease or a set of diseases. A set of diseases are distinguished in next level of
refinements.