Information Technology Reference
In-Depth Information
Attributes and References.
Attributes and references are part of the class
diagram definition. However, they have there values instantiated at the creation
of the process. We translate both attributes and references to parameters passed
during the creation of the translated process. Fig. 7 illustrates this in terms of
a translated route object
R
1, where the input parameters of the process are
presented. Channel
obj chan
is the process associated channel. The
id
attribute
is translated to the
variable. The other channels are references for the
different objects in the system.
route id
proctype R1(chan obj_chan; int route_id; chan point_P1;
1
chan track_T1; chan track_T3; chan signal_S1) {
2
...
3
}
4
Fig. 7.
Process parameters for the route object
R
1
States and Transitions.
In order to keep the state-based structure found in
xUML, we decided to translate regions of a state machine to global variables.
This way, the states became constants in PROMELA that are set to the correct
global variable once the state is changed. Moreover, transitions are translated
to
transition blocks
. A transition block is an entry in a PROMELA condition or
repetition structure. It has a guard, which uses the global variables to match the
current state of the translated process. If a guard is true, other statements corre-
sponding to the actions of the xUML transition are executed. At the end of the
execution of the transition block, the new state is set for the translated process.
Examples of translated
change
and
signal
transitions are shown in Fig. 8.
1
/* Change-Transition */
2
:: atomic { (route_active_active[id] == preparing) &&
(route_route[id] == active) &&
3
((((track_element[0] == automatic) &&
4
(track_automatic_automatic[0] == ready)) &&
5
((track_element[2] == automatic) &&
6
(track_automatic_automatic[2] == ready))) &&
7
(((point_point[0] == normal) &&
8
(point_normal_detected[0] == left))) &&
9
(((signal_element[0] == automatic) &&
10
(signal_automatic_automatic[0] == ready))));
11
assert(nfull(signal_S1));
12
signal_S1!set_proceed;
13
route_active_active[id] = ready;
14
route_route[id] = active;
15
16
}
17
...
18
/* Signal-Transition */
19
:: (msg_name == reserve_route) && (route_route[id] == idle);
assert(nfull(point_P1));
20
point_P1!to_left;
21
route_active_active[id] = preparing;
22
route_route[id] = active;
23
Fig. 8.
Example of
change
and
signal
transitions for route object
R
1
