Information Technology Reference
In-Depth Information
var
t:ttime :
after
(t)
8
[]
9
receive external signal Close()
10
/
further receptions
/
11
od
12
Always taking the minimum time of the next timer due as a waiting time disal-
lows certain behaviors, as is demonstrated in Fig. 4.
StateMachine_0
Signal_1
State_2
State_0
State_1
5
Signal_0
State_3
[ else ] / send_Signal_2
2
[ oclIsInState(State_3) ] / send_Signal_3
State_4
Fig. 4.
Simple State Machine Example with Interdependent Time Triggers
In the example, due to the restriction to move to the next timer firing, a trace
like
ctr Signal_1, obs after(4), ctr Signal_0 ,after(1), obs Signal_3
cannot be taken any longer. Therefore we lose the observation
Signal 3
in the
example. In order to mitigate this shortcoming without the need to enumerate
every time value that is smaller than the time value of the next timer firing, we
propose to add non-deterministic transitions in the UML model that explicate
these additional interleavings. Notice that this might be done on the fly by a
tool that over-approximates such situations and adds the relevant transitions.
5R su s
We have implemented the presented transformations in a tool chain compris-
ing two applications. The first utility takes a UML model and generates the
object-oriented action system code. The second tool (“Argos”) then converts
the OOAS to an action system that is the input for our test-case generator
called “Ulysses” [12,13]. As a second option, Argos is able to generate an im-
plicit labeled-transition system in CADP-style (cf. [14]). All figures in this section
were produced using this second back-end of Argos and the CADP tools.
Table 3 shows some basic figures for three different models of the car alarm
system. The two one-region-only models are branching bisimilar [15] and in-
cluded (modulo branching equivalence) in the multi-region model. Within the
table,
B-Min.
stands for a minimization using strong bisimulation [16], while
W-Min.
stands for a sequence of weak-trace minimization that eliminates all
