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

i f ( PM_Actuator_V == OFF){

/ ∗ Guards No. 2 ∗ /

if (( sp == Pace_Int ) | | (( sp < Pace_Int ) &&

( AV_Count > V_Blank ) && ( AV_Count >= FixedAV ) ) ) {

/ ∗ Guards No. 3 ∗ /

i f (( sp >= VRP)&&(sp >= PVARP) && ( sp >= URI)){

/ ∗ Actions ∗ /
PM_Actuator_V = ON;

last_sp = sp ;
return TRUE;
}}}
return FALSE;

}
...

To make the generated code executable, the EB2ALL tool generates an Iterate
function that contains a list of all functions as in form of a function call. Another
function is a main body of the program like main() in 'C', which calls Iterate func-
tion. These two extra functions are used to compile and execute the generated code.

...
BOOL Iterate (void)
{

if ( Actuator_ON_V()==TRUE ) return TRUE;

if ( Actuator_OFF_V()==TRUE ) return TRUE;

if ( Actuator_ON_A()==TRUE ) return TRUE;

if ( Actuator_OFF_A()==TRUE ) return TRUE;

if ( Sensor_ON_A()==TRUE ) return TRUE;

i f ( Sensor_OFF_A ()==TRUE ) r e t u r n TRUE;

if ( Sensor_ON_V()==TRUE ) return TRUE;

i f ( Sensor_OFF_V ()==TRUE ) r e t u r n TRUE;

if ( tic ()==TRUE ) return TRUE;

if ( tic_AV()==TRUE ) return TRUE;

i f ( Thr_Value_A ()==TRUE ) r e t u r n TRUE;

i f ( Thr_Value_V ()==TRUE ) r e t u r n TRUE;

if ( Hyt_Pace_Updating ()==TRUE ) return TRUE;

if ( Increase_Interval ()==TRUE ) return TRUE;

if ( Decrease_Interval ()==TRUE ) return TRUE;

if ( Acler_sensed ()==TRUE ) return TRUE;

/ ∗ Signal deadlock ∗ /

return FALSE;

}
...

The source code is automatically generated in any programming language (C,
C++, Java and C#) from the verified specification in less than five seconds. The
generated code resulted in over 5000 lines in all operating modes. Here, we have
presented a brief overview of the translation from the Event-B specification of the