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

Ta b l e 9 . 4 Proof statistics

Model Total number of POs Automatic proof Interactive proof

Closed-loop model of one-electrode pacemaker

Abstract model 304 258 (85 %) 46 (15 %)

First refinement 1015 730 (72 %) 285 (28 %)

Second refinement 72 8 (11 %) 64 (89 %)

Third refinement 153 79 (52 %) 74 (48 %)

Closed-loop model of two-electrode pacemaker

Abstract model 291 244 (84 %) 47 (16 %)

First refinement 1039 766 (74 %) 273 (26 %)

Second refinement 53 2 (4 %) 51 (96 %)

Third refinement 122 60 (49 %) 62 (51 %)

Total 3049 2147 (70 %) 902 (30 %)

9.10.3 Proof Statistics

Table 9.4 expresses the proof statistics of the development of the closed-loop model
of the cardiac pacemaker with the heart system. These statistics measure the size
of the model, the proof obligations (POs) generated and discharged by the Rodin
prover and those that are interactively proved. The complete development of the
heart model results in 3049 (100 %) POs, within which 2147 (70 %) are proved
automatically by the Rodin tool. The remaining 902 (30 %) POs are proved inter-
actively using the Rodin tool. Integration of the heart model and the cardiac pace-
maker model generates lots of extra POs. The main reason of these new POs is
to use shared variables in both models to link between the heart and pacemaker
models. A set of invariants corresponding to the shared variables generates new
POs. For example, the current clock counter variable ( sp ) is shared, which has
been used in events of the heart and pacemaker models. The combined invariants
of the heart and pacemaker models generate new POs corresponding to the cur-
rent clock counter variable ( sp ). The whole system represents functional properties
of the cardiac pacemaker operating modes under the biological environment in the
heart. The heart model represents normal and abnormal states of the heart, which
is estimated by the physiological analysis. To guarantee the correctness of these
functional behaviours, we have established various invariants in the incremental re-
finements.
The use of model checker helps to discover some unexpected behaviours, and
assists to verify all the operating modes of the cardiac pacemaker in the heart envi-
ronment model. A tool ProB [ 36 ] is used to animate the closed-loop model and able
to prove the absence of errors.