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

The translation tool uses a similar kind of fashion to translate each event of the
Event-B model. Event-B is a very rich modelling language for representing for-
mal notation of a specification, but translation tool supports only subset of formal
notations of Event-B. Event-B expressions and statements are code generated,
such that the generated code behaves like it is expected from the specification.
A set of translation rules and basic syntactic architecture is defined in Tables 7.2 ,
7.3 and 7.4 . During the code translation process, a run-time exception function
is generated if an undefined expression or an error statement is occurred. A gen-
erated error invokes an exception function, which terminates the code translation
process and reports that an undefined expression into a code generation log file.
The next level of the translation tool presents the scheduling techniques to pro-
duce an executable code.
7.3.6 Events Scheduling
This phase is not producing any translation part of the translation tool. This section
introduces to generate a function for organising all event functions. There are two
ways to organise all the event functions:
1. Optimise : An optimised code is used to make a group of calling event functions
into a new function. An incremental refinement-based structure of events within
an Event-B model provides grouping information about the events. A recursive
algorithm is used in the translation tool to discover structuring information from
current Rodin project, and could exploit it to recursively generate nesting call-
ing a set of functions corresponding to the abstract events. Merging of common
event guards is currently avoided in order to preserve direct mapping between
Event-B statements and translated code, at the cost of possible performance opti-
misations. However, if translatable guards are already placed in an abstract level,
then guards are forming a group of concrete events. An event group is inserted for
execution in place of multiple events for improving the run-time performance.
Figure 7.2 shows a basic architecture of event scheduling using optimisa-
tion approach. This figure represents a tree structure of the refinement develop-
ment, where an abstract model is represented as AM and refinement models are
represented through RM 1 , RM 2 ... , and finally concrete models are represented
by CM . All refinement models ( RM i ) are parts of the single abstract refinement
( AM ). This figure has two groups G 1 and G 2 . G 1 makes a group of a set of
events at first refinement level and G 2 makes a group of events at the second
refinement level. A user can select the refinement level for making a group of
events before code generation. Each group has a set of events, which are only
executable when abstract guards are true . If a user select higher number of re-
finement level for optimisation then the number of groups may be increased. For
instance, in Fig. 7.2 group G 1 has refinement level 1, therefore there are three
possible number of groups, while in the group G 2 has refinement level 2 and
possible number of maximum groups are five corresponding to the number of
blocks in each refinement level.