VTS Language |
|
The basic elements of our graphical notation are points connected
by lines and arrows. Points are labelled by the corresponding
(possibly empty) set of events, meaning that the point stands for
the occurrence of one of these events during execution. An arrow
between two points indicates precedence of the source point with
respect to the destination point. A set of events labelling the
arrow are interpreted as forbidden events between both points. |
A simple introduction to this notation can be found in the
following examples. Fig. 1 shows a VTS pattern
that expresses a predicate about an execution that is true if and
only if it contains a stimulus e followed by two responses r1
and r2 (i.e., the next r1- and r2-events), which are not
separated by another response, r3. Triangles bellow points are
used to assign them an optional name. |
Figure 1. Separated responses |
The arrows from stimulus to response1 and response2 indicate
that stimulus e occurs before responses r1 and r2,
regardless of the relative order between them. To indicate that
the point response1 (respectively response2) is the first
occurrence of its label after e (i.e. there is not another r1
(r2) between e and r1 (r2)), we label with r1 (r2) the
arrow stimulus-response1 (-response2). In order to express
the condition "... which are not separated by another response,
r3", we add a dashed line linking response1 and response2,
labelled with r3. We use a line instead of an arrow because
there is no precedence between response1 and response2 (their
relative order is unimportant). Now we can illustrate when a given
execution matches the VTS scenario of
Fig. 1. Suppose that we have the following sequences
of events: |
s1: | ... a, e, b, c, r1, d, r3, r2, z..., |
s2: | ... a, e, b, c, r1, d, r2, f, r3, z..., |
s3: | ... a, e, b, r2, r1, c, r3, r2, z.... |
|
Then sequences s2 and s3 match the scenario, because the first
r1-event and r2-event after the only e-event have no
r3-event in between. If this should be interpreted as a
negative scenario, we would discard systems producing s2
and s3 for violating our requirement. On the contrary, the
sequence s1 does not match the scenario, and therefore would
satisfy (agree with) the requirement. |
The trained reader should immediately appreciate the simplicity of
this notation over non-graphical alternatives. For example the
following TCTL [ACD93]
formula(*) expresses the same requirement as the
scenario in Fig. 1.
|
|
VTS has the virtue, over this kind of notations, of being
intuitive enough to be used by industry practitioners lacking
academical training, while still possessing a formal semantics and
serving as an input for formal verification methods such as
modelchecking. |
(*) We are using a trick
to predicate on states instead of events as is used in the Kronos
tool [BDM+98]. Another possible technique are
fluents [GM03]. |
Let us introduce now a simple case including temporal constraints.
The scenario of Fig. 2 captures the case
where a stimulus e is not followed by any response within 100
time units (a violation of a bounded response property). The
unlabelled point represents an instant after the stimulus e
occurs. The restriction >100 under the arrow means that the
temporal distance between both is greater than 100 t.u. We express
the absence of events r1 and r2 between stimulus and
instant by labelling the arrow with r1, r2. |
Figure 2. Bounded response |
When scenarios include temporal restrictions, they must be matched
to time-stamped sequences. Let us consider the previous sequences,
with timestamps added to each event (for the sake of simplicity,
we use natural numbers as timestamps, but VTS admits any
non-negative real numbers): |
s4: ... |
a |
e |
b |
c |
r1 |
d |
r3 |
r2 |
z |
..., |
12 |
15 |
39 |
50 |
72 |
123 |
140 |
148 |
155 |
s5: ... |
a |
e |
b |
c |
r1 |
d |
r2 |
f |
r3 |
z |
..., |
3 |
7 |
12 |
88 |
109 |
111 |
114 |
121 |
125 |
152 |
s6: ... |
a |
e |
b |
r2 |
r1 |
c |
r3 |
r2 |
z |
..., |
5 |
7 |
69 |
78 |
87 |
100 |
146 |
152 |
199 |
|
Sequence s5 matches the anti-scenario of
Fig. 2, because neither an r1-event nor a
r2-event appears after e for 100 t.u., thus violating the
bounded response requirement. On the other hand, sequences s4
and s6 do not match the (negative) scenario, so they satisfy the
requirement. |
We now have the elements to describe a more complex requirement: a
correlated response. Fig. 3 shows a
VTS pattern for the violation of the requirement that
whenever two responses follow a given stimulus e
(i.e., the next r1, r2 labelled events) they should be separated by at least 20 t.u. and at most 100 t.u.
As in Fig. 1, the arrows indicate the relative
ordering between e, r1 and r2. In this example we introduce
an abbreviation to represent a frequent sub-pattern: there is no
other r1-event between e and a particular r1-event (i.e.
certain point represents the next occurrence of r1 after
e). The abbreviation is a second (open) arrow near r1, and is
equivalent to adding r1 as a forbidden event on the arrow (as we
did in Fig. 1). The temporal constraint is expressed
as ¬[20,100] on the dashed line between the responses.
Conversely, in order to express that there is not another
e-event after a particular e and before an r1-event (i.e. to
signal the previous e-event before r1) a symmetrical
notation can be used: an open arrow near the e extreme. |
Figure 3. Correlated responses |
Returning to sequences s4, s5 and s6, it can be seen that
s4 does not match the scenario in
Fig. 3, because the temporal distance
between the r1 and the r2-events (148 - 72 = 76 t.u.) is not
in the time span ¬[20,100]. The opposite happens for s5
with inter-responses distance equal to 114 - 109 = 6 t.u. and
s6, with 87 - 78 = 9 t.u. |
Another useful idiom asserts that something happens (or not) since
the beginning or until the end of a given execution. For these
situations, VTS has two special symbols: a big full circle
for begin, and two concentric circles for end. For
example, we show in Fig. 4 a scenario stating that
the temporal distance between the first a and the last b (both
in the whole execution) is limited to 100 t.u. |
Figure 4. Begin and end symbols |
VTS can also identify the
first or the last in a
(possibly unordered) set of events. In the graphical notation, the
first event in a set is represented by a point linked to each
point in the set by dotted lines ending in small empty circles. A
similar notation is used for the last event, but using a small
full circle. Nested combination of first and last representatives
are allowed, as can be seen in Fig. 5. Part of this
scenario will match situations where, given two set of events,
{a1,a2} and {b1,b2,b3}, the temporal distance between the
last event in each set to occur is less than 100 t.u.
Fig. 5 also shows how VTS can convey very
complex properties of a system. This scenario depicts the case
where a watchdog is turned on (wd-on) at least 50 t.u. before
any event in both sets occurs and not turned off until all
monitored events occur. This watchdog is supposed to detect the
case described above (certain time spread between the first and
the last group to end). As this is a negative scenario, it matches
(faulty) traces in which all these conditions are met and yet the
watchdog fails to issue such an alarm. |
Figure 5. Representatives |
The next table summarizes the complete graphical
notation of VTS. |
|
|