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

Fig. 9.10 The electrical conduction and landmarks of the heart system

nodes, which constitute the impulse propagation path. The impulse propagation time
and impulse propagation velocity for each pair of nodes vary due to different types
of muscles in the heart. To formalise the heart system, we define three constants im-
pulse propagation time ConductionTime , impulse propagation path ConductionPath
and impulse propagation velocity ConductionSpeed . All these constants are initial
components, which are defined through a set of axioms ( axm 1- axm 4).
To formalise the cardiac pacemaker, we define a set of constants ( LRL , URL ,
ARP , VRP , PVARP , etc.), which expresses timing intervals. These timing intervals
are used as a set of configuration parameters. To model boolean behaviour of the
sensor and actuator, we define an enumerated set status . A set of axioms for the
cardiac pacemaker is defined in axm 5 and axm 6. All these constants and axioms
have been extracted from the technical specification [ 7 ], which are validated by the
cardiologist and the physiologist.

axm 1 : partition(ConductionNode, { A } , { B } , { C } , { D } , { E } , { F } , { G } , { H } )

axm 2 : ConductionTime ∈ ConductionNode → P ( 0 .. 230 )

axm 3 : ConductionPath ⊆ ConductionNode × ConductionNode

axm 4 : ConductionSpeed ∈ ConductionPath → P ( 5 .. 400 )

axm 5 : LRL ∈ 30 .. 175 ∧ URL ∈ 50 .. 175 ∧ PVARP ∈ 150 .. 500

axm 6 : ARP ∈ 150 .. 500 ∧ VRP ∈ 150 .. 500 ∧ status ={ ON, OFF }

To define an abstract model of the closed-loop system, we develop the combined
model of the cardiac pacemaker and heart, where the cardiac pacemaker acts accord-
ing to the heart behaviour. The environment model of the heart behaves according