This use case has been submitted as a verification challenge at the 6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems [WATERS15]; The specifications for this use case can be found HERE.
We provide different models for each questions of the challenge. We
assume that you have already
installed Tina and
the Fiacre
compiler, frac
. Tina is necessary in order to open
files with the
extension .ndr
, .net
, .ktz
and .scn
. The tina distribution also provides the
tool tina
and sift
for generating a model
state space.
Simple TPN Model of the Video Tracking System
Our first model is a simple version of the specification, using Time Petri Net (TPN), without distinctions between frame ids and for a buffer of size 1. The timing constraints corresponds to the set of values WIDE defined in our article [WATERS15]
Files with the extension .ndr
are a graphical
representation of a TPN. They can be opened in the nd
tool; this is an editor and TPN simulator that is part of the Tina
distribution. Below we show a screenshot of the file opened
in nd
and using the stepper tool. To open the
simulator, just go to the menu toolbar in nd
,
under Tools > stepper simulator
.
We also provide a more complex version of the net that can be used
to prove that frame ids can be lost. This is a model where we
alternatively generate frames with the id 0
or 1
.
A place has been added to this net (called p0
in the
model) where a token is placed every time a frame with id 0 is
generated (transition t23
) and consumed every time a
frame with this id is displayed. Hence we can loose a frame if the
place p0
can have more than one token. This can be
checked by calling tina directly from nd
. Just go to
the menu toolbar, under Tools > reachability analysis
(see screenshot below) and specify a limit on the number of tokens
in a place (pbound
).
Boundedness of the net can be checked using the command-line
tool sift
with the option (flag) -b
. This
is the recommended way of using the rest of our examples. You can
check
the documentation
for the Tina toolset or simply have a look at the
Manual
Reference Pages of sift
to see the different
options available. (We use the symbol $>
for the
shell prompt.)
$> sift -b 1 looseframe.ndr
marking bound overflow for place p0
Time Petri Net Solution (buffer of size 1)
Computing the Minimal and Maximal Latency (Best and Worst Case End-to-End Delay)
We provide a TPN model for checking the maximal latency (Worst Case Traversal Time) of the system.
The net has an extra transition labeled DEADLINE
(transition t25
) than can fire 411 u.t. (units of time)
after a frame has been generated (in
transition t23
). Hence the maximal latency is bigger
than 411 if it is always the case that, when the frame is displayed
(transition t19
, labeled DISPLAY
), there is
still a token in place p18
. This can be checked on the
model using the invariant t19 => p18
.
$> sift -M -f "t19 => p18" maxlatency-wider.ndr
378 marking(s), 31379 domain(s), 6482 classe(s)
0.546s
Model-checking takes less than a second (0.546s) on our testing
machine using the option -M
(Intel64, 2.3GHz, Windows
with 8GB RAM). The same invariant takes approx. 250s with the
default state space abstraction (that preserves LTL properties).
The same model with a timing constraint of 411 for
the DEADLINE
transition gives a counter-example (the
invariant is false). If we take into account the scaling factor
applied on our timing constraints (and add the 10ms for displaying
the image) this gives a maximal latency of 147ms.
$> sift -M -f "t19 => p18" maxlatency-wider.ndr
386 marking(s), 24255 domain(s), 6824 classe(s)
some state violates condition -f:
p10 p13 p16 p17 p3 p7
firable: t19 t12
0.452s
The counter examples provides an execution trace (a sequence of
transitions) that corresponds to the maximal latency. On the WIDE
set of constraints, it is easy to generate an example and to run it
in the stepper simulator of nd
. For this, in the
stepper mode of nd, just go to File > open history
and
load the file maxlatency-wider.scn
. (This trace
corresponds to the shortest--in number of
transitions--counter-example.)
A cursory glance at the counter-example already gives some interesting information. Indeed it appears that, for this "slowest case", task T1 executes at the slowest possible period, task T4 executes at the fastest possible period, until the offset between the two periods is greater than the period of T3. This is also the situation leading to a loss of frame.
Following a similar approach, we also provide a TPN model for checking the minimal latency of the system. This example use the set of timing constraints EXACT defined in [WATERS15].
Fiacre Solution (buffer of size CAPACITY = 3)
Our second set of solutions to the challenge use the Fiacre
specification language. We provide a first solution in the
file looseframe.fcr
below.
- looseframe.fcr
- Makefile
- Makefile (Windows version)
In order to generate (and explore) the state space of a Fiacre
model, the fiacre file (extension .fcr
) must be
compiled into one of the input format of Tina. You can find some
information on the
following documentation
page. Basically, it is necessary to generate a TTS model
(actually a folder with the extension .tts
) using
the frac
tool and then to compile the C file contained
in the TTS folder into a shared library.
To simplify this task we provide a Makefile
. You must
edit the Makefile to specify the path to your local installation of
Fiacre (variable FRACLIB
) and the type of operating
system (variable HOSTTYPE
; then run the following
command:
$> make looseframe.tts
The Tina toolset provides a stepper simulator for TTS files
called play
. (type the command h
to obtain
some help.)
$> play looseframe.tts
The file looseframe.tts/looseframe.ltl
contains LTL
formulas that corresponds to the properties defined in the Fiacre
model. These formulas can be checked using selt
, the
LTL model-checker distributed with the Tina toolset. In our case we
have two properties: property maxident
states that the
frame id 6 is never used in the model (at any moment, we need at
most 6 different frames); property looseframe
states
that it is not possible to loose a frame (to fire the transition
containing the tag #looseframe
at line 132 of our
FIacre model).
op maxident = [] (- ((C_w1)));
pop looseframe = [] (- ((T3_1_t1)));
For verification and state space exploration, TTS files can be used
by tina
and selt
just
like .ndr
files. Since we only need to check safety
properties, we can use option -f
of sift.
sift -M .\looseframe.tts -f "- C_w1"
sift -M .\looseframe.tts -f "- T3_1_t1"
Property maxident
is true (checked in 19.375s on our
test machine) while property looseframe
is false (a
counter-example is found in 0.468s). (Valid properties are a
worst-case scenario for verification since it means that we need to
generate the whole state space.)
Computing the Minimal and Maximal Latency (Best and Worst Case End-to-End Delay)
We provide two different models for computing the best and
worst-case latency (both examples are coded with the set of
constraints WIDE). The size of the buffer is defined by a constant
called CAPACITY
; its value is set to 3 in our
examples.
Our modeling approach is similar for both models. We use a special
frame (a value of type frameid
called MAGIC
) that is tracked by a process
called observer
. The observer enters the
state deadline
when the special frame is generated. For
the maximal latency, we check if the observer is still in state
displayed when the frame is displayed.
property max is ltl [] ((C/5/tag displayed) => (C/6/state
deadline))
In our example we use the value 411 in the timing constraint of the
deadline (last integer value for which the property max
is false).
$> make maxlatency.tts
$> more .\maxlatency.tts\maxlatency.ltl
$> sift -M -f "(((T4_1_t2) => (observer_1_sdeadline)))" maxlatency.tts
Computing the Minimal Time Between Two lost Frames
We provide a separate model for the last question of the challenge. In this example, we fix the value of T1 period at 39.66ms, the period of T3 at 13.33ms and the period of T4 at 40.33ms. (Note that these periods are not in the range of possible values given in the specification and called SPEC in our paper.)
In this model, we generate two special frame ids
(MAGIC1
and MAGIC2
) separated by a fixed
number of periods of the task T1. The number of periods is defined
by the constant COUNT
. We use a
tag, #twolosses
, to declare the transition
corresponding to the loss of these two frames.
$> make between2lost.tts
$> more .\between2lost.tts\between2lost.ltl
$> sift -M -f "- T4_1_t4" between2lost.tts
We find that the property is true for a difference of 112 periods but false for 111 periods. Hence the solution, for the given values of the periods, is 4.4s.
Files Available on this Use Case
Everything in a single archive file.
TPN files
Scenarios files
Fiacre files
- Makefile
- Makefile (Windows version)
- looseframe.fcr
- maxlatency.fcr
- minlatency.fcr
- between2lost.fcr
References
[WATERS15] Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina. B. Berthomieu, S. Dal Zilio and D. Le Botlan, 6th International WATERS Workshop.