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

9.8 Formal Development of the Two-Electrode Cardiac
Pacemaker

9.8.1 Context and Abstract Model

In this section, we describe the formal development of initial modes of the two-
electrode pacemaker system using the basic notion of action-reaction and real-time
constraints, to focus on pacing and sensing activities of the pacemaker's actuator
and sensor. The initial context of the two-electrode pacemaker is similar to the one-
electrode pacemaker. We give here only newly defined constants and axioms. A new
constant atrioventricular (AV) interval (FixedAV) is defined in axm 8. Refractory pe-
riod constants Atria Refractory Period (ARP), Ventricular Refractory Period (VRP)
and Post Ventricular Atria Refractory Period (PVARP) are defined by axioms ( axm 9,
axm 10 and axm 11). Another new constant V _ Blank is defined as blanking period
as an initial period of VRP. Finally, we introduce some basic initial properties using
defined constants of the system by axioms ( axm 13, axm 14 and axm 15).

axm 8 : FixedAV ∈ 70 .. 300

axm 9 : ARP ∈ 150 .. 500

axm 10 : VRP ∈ 150 .. 500

axm 11 : PVARP ∈ 150 .. 500

axm 12 30 .. 60

axm 13 : URI > PVARP
axm 14 : URI > VRP
axm 15 : VRP ≥ PVARP

: V _ Blank ∈

Abstraction of DDD Mode

In the two-electrode pacemaker system, the pacemaker delivers a pacing stimulus
in both atrial and ventricular chambers. In DDD operating mode, the first letter 'D'
represents that the pacemaker paces in both atrial and ventricle chambers; second
letter 'D' represents that the pacemaker senses intrinsic activities from both atrial
and ventricle chambers and final letter 'D' represents two conditional meaning that
depends on atrial and ventricular sensing; first is that atrial sensing inhibits atrial
pacing and triggers ventricular pacing and second is that ventricular sensing inhibits
ventricular and atrial pacing [ 22 , 35 ].
Two new variables PM_Actuator_A and PM_Actuator_V are defined that repre-
sent ON or OFF state of the pacemaker's actuators for pacing in both atrial and ven-
tricular chambers. Similarly next two variables PM_Sensor_A and PM_Sensor_V
represent ON or OFF state of the pacemaker's sensor for sensing an intrinsic pulse
from both atrial and ventricular chambers. An interval between two paces is de-
fined by a new variable Pace_Int that must be between upper rate interval (URI)
and lower rate interval (LRI), is represented by an invariant ( inv 5). A variable sp