fiacre logo

Fiacre Use Case

An Aerial Video Tracking System

 laas logo

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.

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

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.