EB2ALL: An Automatic Code Generation Tool - Using Event-B for Critical Device Software Systems - page 132

objM1_VOOR . I t e r a t e ( ) ;
}
}

}

In the Java language ...

public static void main( String [] args )

{
M1_VOOR objM1_VOOR = new M1_VOOR ( ) ;

i f ( objM1_VOOR . INITIALISATION ()== t r u e ){

try{
for ( i n t n=0;n<=1000;n++){
objM1_VOOR . I t e r a t e ( ) ;
}
}catch ( Exception e){
e . printStackTrace ();
}
}

}

7.3.7 External Code Injection and Code Verification

This is also an important phase of the code generating process, where the source
code files have been generated from Event-B specification. This phase provides a
way to introduce some handwritten code or introduction of implicit functions in the
form of an interface in order to compile and run the application in target languages
(C, C++, Java, C#). For example, when a function is defined abstractly and function
returns output value using a set of calculation or algorithms. In that case, a user
requires to write a function body, which is generated by the translator. Thus, the
user has to write a target language function definition for the operation and add it to
the function body of the generated file. To provide some code interface through user
intervention, we have introduced code verification step. The code verification is a
very important step to verify the correctness of an automatic generated code. This
step is required due to manual insertion of an external code. We have considered
following two main objectives for adding external codes in the generated codes:

• If some part of the implementation code is not supported by the code generator;

• The user wants to implement some existing components more efficiently.

Due to the complex architecture of the software-development process, it is im-
possible that any modelling tool can generate directly an executable application.
In large software, different kinds of languages are used for designing final soft-
ware. So, we have provided a facility of code injection. For instance, addition of
hardware specific code (i.e. assembly code) into Event-B generated code. For ex-
ample, in pacemaker case study, Sensor and Actuator are specific hardware units,