IMITATOR

IMITATOR: Experiments Data for AVoCS + FMICS 2017

Case Studies Related to "A unified formalism for monoprocessor schedulability analysis under uncertainty"

This page is dedicated to the case studies related to the manuscript A unified formalism for monoprocessor schedulability analysis under uncertainty by Étienne André.

Software used

IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR 2.9.1 (branch master, build 2259, GitHub hash 5c52978).

Download

genSched

In order to generate the scheduler, we implemented a Python script genSched.py.

The script takes as arguments the list of task names with their tentative maximum number of instances, in the form: task1:nb_instances,task2:nb_instances… (where task1 is the highest-priority task)

An example of call is therefore:

> python genSched.py R:2,S:4,Q:5,P:5

This yields a skeleton file in the IMITATOR input format, to which the actual PTaskA needs to be added.

Case studies

We present in the following table a list of experiments performed using IMITATOR.

The model for each PTaskA can be obtained by clicking on the specification name; logs including results can be obtained by clicking on the response time column; the actual result by IMITATOR (in the IMITATOR normalized form) can be obtained by clicking on the "result"; a graphical 2D representation of the synthesized constraint can be obtained by clicking on the [g] (when available). Columns A, L, T, X, P denote the number of automata, of locations, of tasks, of clocks and of parameters respectively. These figures are given both for the task automaton, and for the global system (which includes the translation of the scheduler into an additional automaton).

The experiments are ordered as in the paper.

Some additional experiments that could not fit into the paper due to space concern are marked with "*".

PTaskA Full model Analysis Result
Name Ref |A| |L| |T| |X| |P| |A| |L| |X| |P| Type t (s) Result Graphics
Fig.1 [FKPY07] 1 4 4 1 0 2 12 21 0 Non-parametric schedulability 0.55 s Schedulable
Fig.1 t0>t1>t2>t3 [FKPY07] 1 4 4 1 0 2 12 21 0 Non-parametric schedulability 0.12 s Non-schedulable
Fig.2 [FKPY07] 1 4 4 1 1 2 8 13 1 Parametric schedulability (p') 0.13 s Part. schedulable
Fig.2 [FKPY07] 1 4 4 1 1 2 8 13 1 Parametric schedulability (p) 0.96 s Part. schedulable
Fig.2 [FKPY07] 1 4 4 1 2 2 8 13 2 Parametric schedulability (p + p') 6.82 s Part. schedulable [g]
Fig.1* [FKPY07] 1 3 2 2 1 2 21 21 1 Parametric schedulability (p') 0.64 s Part. schedulable
Fig.1 [FKPY07] 1 3 2 2 1 2 12 21 1 Parametric schedulability (p) 4.22 s Part. schedulable
Fig.1 [FKPY07] 1 3 2 2 2 2 12 21 2 Parametric schedulability (p + p') 4.91 s Part. schedulable [g]
Fig.1 [FKPY07] 1 3 2 2 1 2 12 21 1 Robust schedulability 1.26 s Non-robust
Fig.1 [FKPY07] 1 3 2 2 2 2 12 21 2 Robust + parametric schedulability (p) 24.2 s Part. robust sched. [g]
Fig.1* [FKPY07] 1 3 2 2 3 2 12 21 3 Robust + parametric schedulability (p + p') 38.5 s Part. robust sched. [g]

Description of the Case Studies

Both case studies are variants of 2 benchmarks of [FKPY07].

Algorithms used

For all case studies, the following command was used:

> imitator case_study.imi -mode EF -merge -incl -output-result -output-cart

References

[AFKS12]
Étienne André, Laurent Fribourg, Ulrich Kühne and Romain Soulat. IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems. In Dimitra Giannakopoulou and Dominique Méry (eds.), FM’12, LNCS 7436, Springer, pages 33–36, August 2012. (English) [PDF | PDF (author version) | BibTeX]🌐
[FKPY07]
Elena Fersman, Pavel Krcál, Paul Pettersson, Wang Yi: Task automata: Schedulability, decidability and undecidability. Inf. Comput. 205(8): 1149-1172 (2007)

Contact

Étienne André