Information Technology Reference
In-Depth Information
process (
Proctype
). The first lines are used to define the name of the rule (line
1), specify the original element being transformed (UML class, line 2) and to
what element it is being mapped to (PROMELA
Proctype
, line 3). This informs
the transformation engine that for every class element in the UML model, this
rule must be called. However, we specify a guard (line 6) stating that any class
with the name
application
shall not be transformed. The
application
class defines
the initial scenario and is transformed in a different rule.
The name of the class is maintained in the target process element (line 9).
If the class diagram has generalisations (line 15), it makes sure that they are
translated as well (lines 20 and 22). The function
equivalent()
is used to trigger
an implicit rule. This way, if the super class has not been transformed yet, its
transformation rule is triggered in order to set the correct references in the
target model. We also translate the messages that a class can receive (lines
30 to 34) in order to correctly build the environment. Finally, we define three
different operations that are used for translating attributes and references (line
37), states and state variables (line 40) and the transition blocks obtained from
the associated state machine (line 43).
5.3 PROMELA Models to PROMELA Code
The Epsilon Generation Language (EGL) is used to generate the verification
code starting from the obtained PROMELA model. In EGL definitions, we de-
fine templates of the final text (which are not to be changed) and specify dy-
namic structures used to add information gathered from the model. This way, we
have specified in total, four different templates. They are used for declaring the
[%
1
for (p in ProctypeDef.allInstances) {
2
var s;
3
%]
4
proctype [%=p.name%](chan obj_chan[%=p.generateParameters()%]) {
5
atomic {
6
mtype msg_name;
7
int id = [%=p.id%];
8
[%=p.initialStates()%]
9
}
10
do
11
[%=p.transitionBlocks()%]
12
[%=p.changeTransitionBlocks()%]
13
[%=p.timeTransitionBlocks()%]
14
::atomic { timeout && nempty(obj_chan);
15
obj_chan?msg_name;
16
[%=p.signalTransitionBlocks()%]
17
}
18
od;
19
20
}
21
[%
22
}
23
%]
Fig. 13.
EGL rule for generating translated processes in PROMELA
