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

Ta b l e 9 . 3 Proof statistics

Model Total number of POs Automatic proof Interactive proof

One-electrode pacemaker

Abstract model 203 199 (98 %) 4 (2 %)

First refinement 48 44 (91 %) 4 (9 %)

Second refinement 12 8 (66 %) 4 (34 %)

Third refinement 105 99 (94 %) 6 (6 %)

Two-electrode pacemaker

Abstract model 204 195 (95 %) 9 (5 %)

First refinement 234 223 (95 %) 11 (5 %)

Second refinement 3 3 (100 %) 0 (0 %)

Third refinement 83 74 (89 %) 9 (11 %)

Total 892 845 (94 %) 47 (6 %)

potential problems, to improve invariant's expressions in our Event-B models, for
instance, by generating counter-examples when it discovers an invariant violation.
ProB may help in improving invariant expression by suggesting hints for strength-
ening the invariant and each time an invariant is modified; new proof obligations are
generated by the Rodin platform. It is the complementary use of both techniques to
develop formal models of critical systems, where high safety and security are re-
quired. More errors are corrected during the elaboration of the specifications while
discharging the proof obligations and careful cross-reading than during the anima-
tions. We have validated all operating modes of the pacemaker in each refinement
of models. The pacemaker specification is developed and formally proved by the
Rodin tool.
ProB was very useful in the development of the pacemaker specification, and was
able to animate all of our models and able to prove the absence of error (no counter
example exist). The ProB model checker also discovered several invariant viola-
tions, e.g., related to incorrect responses or unordered pacing and sensing activities.
It was also able to discover a deadlock in two of the models, which was due to the
fact that “clock counter” were not properly recycled, meaning that after a while no
pacing or sensing activities occur into the system. Such kind of errors would have
been more difficult to uncover with the prover of Rodin tool.
Table 9.3 is expressing proof statistics for the formal development of the pace-
maker using the Rodin platform. These statistics measure the size of the model, the
proof obligations generated and discharged by the Rodin prover, and those are in-
teractively proved. The complete development of the pacemaker system results in
892 (100 %) proof obligations, in which 845 (94 %) are proved automatically by the
Rodin tool. The remaining 47 (6 %) proof obligations are proved interactively using
the Rodin tool. In the Event-B models, many proof obligations are generated due to
the introduction of new functional behaviours and their parameters (threshold, hys-