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

A new event Change_Pace_Int is introduced to update the current value of the
pace interval. This event is defined abstractly, which is used in further refinement
levels to modify the pace interval according to the introduction of different operating
modes like hysteresis and rate modulation . This event represents that when the pace
changing flag ( Pace_Int_flag ) is TRUE then the pace interval ( Pace_Int ) can be
chosen from URI to LRI range.

Abstraction of AAI and VVI Modes

In the abstract model of AAI and VVI modes, all the constants, variables and events
are common as the abstract model of AOO and VOO modes. In this section, we
introduce only extra added new constants, variables and events. We introduce a new
constant refractory period RF ( Atria Refractory Period ( ARP ) or Ventricular Re-
fractory Period ( VRP )) that represents a period during which pacemaker timing in
the heart chamber is not affected by events. Two new axioms ( axm 1, axm 2) are in-
troduced in this abstract level. The first axiom ( axm 1) represents a refractory period
as a constant and the second axiom ( axm 2) represents a static property.

axm 1 : RF ∈ 150 .. 500

axm 2 : URI > RF

A new variable Pace_Sensor as a pacemaker's sensor, is defined as an enumerated
type that represents the presence or absence of sensing pulse from the heart chamber
and a variable last_ss represents the last interval (in ms) between two sensed pulses.
Some new invariants are added here that are common to all other operating modes
(except AOO and VOO) of the pacemaker system. An invariant (inv 3 ) states that
the interval between two sensed pulses is greater than or equal to the refractory
period RF and less than or equal to the pace interval ( Pace_Int ). Invariants ( inv 4,
inv 5) state that the pacemaker's sensor and actuator are always in OFF state during
the refractory period RF . These are the essential safety properties for the refractory
period during which the pacemaker timing must not to be affected by any events that
occur. The last invariant ( inv 6) states that when pace changing flag ( Pace_Int_flag )
is FALSE, current clock counter ( sp ) is greater than the refractory period ( RF ) and
less than the pacing interval ( Pace_Int ), then the pacemaker's sensor should be ON,
means the pacemaker's sensor is ON and continuously sensing the intrinsic activities
from the heart chamber within an alert period ( Pace_Int

− RF ).

inv 1 : Pace _ Sensor ∈ status

inv 2 : last _ ss ∈ N

inv 3 : last _ ss ≥ RF ∧ last _ ss ≤ LRI

inv 4 : sp < RF ⇒ Pace _ Sensor = OFF

inv 5 : sp < RF ⇒ Pace _ Actu = OFF

inv 6 : Pace _ Int _ flag = FA L S E ∧ sp > RF ∧ sp ≤ Pace _ Int ⇒

Pace _ Sensor = ON