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.
 
Search WWH ::




Custom Search