Information Technology Reference
In-Depth Information
The guard of a translated
change
-transition (lines 2 to 16) is composed of
global variables checking the correctness of: (a) the source state of the translated
process (lines 2 and 3); and (b), the other states of translated processes (lines 4
to 11). Amongst the actions, the translated process can generate a message (line
13), although before sending a message it checks if the target channel is not full
(line 12), maintaining the atomicity of the whole transition. Finally, it sets the
target state by changing the values of the global variables (lines 14 and 15). A
translated
signal
-transition (lines 19 to 23) is similar to the
change
-transition.
The only difference is that it incorporates a message name (
msg name
), which
is the signal triggering the transition (line 19).
4.2 The Initial Scenario
In Fig. 3 the definition of a scenario uses the action grammar of the xUML lan-
guage in order to create the objects and define their references. We translate an
initial scenario of xUML (the
application
class and its associated state machine)
to a special PROMELA initial process.
A part of a translated PROMELA initial process, describing only the trans-
lation of the track object
1, is presented in Fig. 9. In the translation, the
initial process has three different purposes. Firstly, it creates the channel that
is associated to the translated object (line 3). Then, it creates the process by
passing as parameters the associated channel and, if necessary, other channel
references needed by the process (line 5). Both the creation of the channels and
the processes occur atomically (lines 2 to 7).
The final purpose of the initial process is to generate inputs from the envi-
ronment for the execution of the verification scenario. Therefore, it enters in an
atomic loop (lines 8 to 19) that has only one guard (line 9) stating that the
system can no longer execute (
timeout
keyword) and all the other channels as-
sociated to translated processes are empty (
empty
function). Once this guard
T
init {
1
atomic {
2
chan T1_ = [5] of { mtype };
3
...
4
run T1(T1_);
5
...
6
}
7
do
8
:: atomic { timeout && empty(T1_) && ...;
9
if
10
::(track_track[0] == free) -> T1_!occupied;
11
::(track_track[0] == occupied) -> T1_!free;
12
::(track_track[0] == free) -> T1_!automatic;
13
::(track_element[0] == automatic) -> T1_!manual;
14
::(track_element[0] == manual) -> T1_!automatic;
15
...
16
fi;
17
}
18
od;
19
20
}
Fig. 9.
Partial PROMELA initial process for the Micro model
