Information Technology Reference
In-Depth Information
of the system. In our translation, every object becomes a PROMELA process,
which we call a translated process. Every translated process has an associated
channel, which is used to receive messages sent from other translated processes,
and the environment. Since generalisation is allowed in the xUML model, we
need to cope with inheriting the behaviour of state machines from super classes.
We tackle this problem by translating all the possible transitions from the class
and its super classes into a single translated process, flattening the structure
of the xUML object. With the intent to preserve the xUML behaviour, every
translated process has the basic structure shown in Fig. 6.
According to this structure, a translated process enters in a loop (lines 1 to 17).
There are two types of guards in this loop: guards used for translated
change
and
after
transitions (lines 2 to 7), and the guard found in line 8, which only becomes
enabled when the
timeout
keyword is true and the translated process has mes-
sages in its associated channel (
nempty
function). Once this guard is enabled, the
translated process gets a message from its associated channel (line 9) and tries to
find a
signal
-transition that is triggered by that particular message (lines 11 to
13). Note that all the actions from lines 8 to 16 occur atomically.
do
1
::
/* Change-Transition 1 */
2
...
3
::
/* Change-Transition N */
4
:: timeout && ...
/* Time-Transition 1 */
5
...
6
:: timeout && ...
/* Time-Transition N */
7
:: atomic { timeout && nempty(obj_chan);
8
obj_chan?msg_name;
9
if
10
::
/* Signal-Transition 1 */
11
...
12
::
/* Signal-Transition N */
13
::else -> skip;
14
fi;
15
16
}
17
od;
Fig. 6.
Basic structure for translated xUML objects
As presented in Subsection 2.2, the
timeout
keyword only becomes true when
the system gets to a deadlock stage where no more transitions can occur. The
basic idea for encoding the xUML behaviour in PROMELA is as follows. The
system starts and tries to apply all possible
change
-transitions in the different
translated processes. Once all
change
-transitions have occurred, the system gets
to a deadlocked situation and the
timeout
keyword becomes true. At this stage, it
may happen that translated processes have messages in their associated channels
(guard in line 8 becomes true). This leads to the translated process trying to apply
signal
-transitions, and the
timeout
keyword becoming false. The applied
signal
-
transition may generate new
change
-transitions in the system. The system enters
the cycle once again, waiting for inputs to occur. There may be a case where no
translated processes have messages in their buffer and the system stops. In this
case, the initial process emulates the environment by generating a nondetermin-
istic input to the system. Below we describe in more details how specific xUML
components are translated to PROMELA.