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

enum s t a t u s {ON, OFF } ; / ∗ Enumerated d e f i n i t i o n ∗ /

c o n s t i n t FixedAV =90; / ∗ Integer in range 70 − 300 ∗ /

const int LRL=60; / ∗ Integer in range 30 − 175 ∗ /

const int ARP=200; / ∗ Integer in range 50 − 175 ∗ /

const int URL=120; / ∗ Integer in range 50 − 175 ∗ /

const int VRP=250;

const int PVARP=150;

const int V_Blank=50;

...
enum s t a t u s PM_Actuator_V ; / ∗ Enumerated type variable ∗ /

enum s t a t u s PM_Sensor_V ; / ∗ Enumerated type variable ∗ /

unsigned long int Thr_V; / ∗ Integer in range undefined ∗ /

u n s i g n e d long i n t AV_Count ; / ∗ Integer in range undefined ∗ /

BOOL AV_Count_STATE ;
unsigned

long last_sp ;

unsigned long int sp ;

unsigned long int Pace_Int ;

...

A set of functions are extracted equivalent to a set of events of the pacemaker
formal model. All the events of Event-B are translated into equivalent program-
ming language functions. An event INITIALISATION is a programming language
function, which initialise default values of all the variables. An event of Event-B
model has fixed organisation of the internal components; local variables, guards
(pre-conditions) and actions. An event may contain some local variables. The global
constants and variables are declared on the top of the programming language source
file, while local variables are declared within the function body. All events of a for-
mal model is translated as a set of programming language functions. This function
has the similar structure as an event. During the translation of the events, the guards
are translated into equivalent to 'if' statement using logical conjunction, disjunc-
tion, implication and equivalence. Each guard represents into a separate 'if' state-
ment like nested 'if' structure. All these guards represent a set of preconditions,
which are required to satisfy for executing the action predicates. All action predi-
cates of a formal model event are directly translatable equivalent into programming
language assignment expressions. The EB2ALL tool is capable to analyse the syn-
tax of Event-B guards and actions predicate. In the cardiac pacemaker formal model,
their predicates are simple, which are obtained through several refinements. All pre-
conditions or guards are required to be TRUE for executing all actions. However,
despite being a complex system, the pacemaker pre-conditions are fairly simple to
calculate. If all the guards are true, then the action's predicates execute and return
TRUE for successful execution of the function. If any 'if' condition false, then the
function returns FALSE and action's part of the function does not execute.

...
BOOL Actuator_ON_V ( void )
{

/ ∗ Guards No. 1 ∗ /