IMITATOR

IMITATOR: Experiments Data for FM 2012

Case Studies Related to the Tool Paper on IMITATOR 2.5 (2012)

This page is dedicated to the case studies related to the manuscript IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems by Étienne André, Laurent Fribourg, Ulrich Kühne and Romain Soulat, published in the proceedings of FM’12, LNCS 7436, Springer, pages 33–36, August 2012 [AFKS12].

IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR 2.5.0.

Version Sources Binary (32 bits) Binary (64 bits) User manual
IMITATOR 2.5.0 [imitator-2.5.0.tar.gz] [imitator-2.5.0-bin32.tar.gz] [imitator-2.5.0-bin64.tar.gz] [PDF]

Binaries have been compiled using KUbuntu 12.10, and should be used on all Linux-like systems.

Case studies and results

We present in the following table a list of case studies computed using the inverse method, as implemented in IMITATOR 2.5.

We give from left to right the name of the case study (with a link to the IMITATOR model), the reference, the reference valuation file pi0, the number |A| of automata in parallel, the number |X| of clocks, the number |P| of parameters, the number |S| of states computed, the number |T| of transitions computed, the number n of iterations of the inverse method, the number |K| of inequalities within the resulting constraint K, the computation time t in seconds (excluding the generation of the graphical outputs), the file containing the resulting constraint, the file containing the description of all states, and the trace set given under a graphical form.

All experiments were performed on a machine equipped with an Intel Core I7 processor with 2.66GHz and 4GiB RAM, running operating system XUbuntu 12.04 (64 bits version).

Case study Reference Pi0 |A| |X| |P| |S| |T| n |K| t Log States Trace set
Tasks chain [SGL97] task_chain.pi0 8 15 21 215 264 16 17 15.5s task_chain.log task_chain.states task_chain.jpg
CPR08 [CPR08] cpr08.pi0 4 6 3 369 485 30 4 6.3s cpr08.log cpr08.states cpr08.jpg
LPPRC 10 [LPPRC10] hppr10_audio.pi0 3 4 9 31 40 12 8 0.162s hppr10_audio.log hppr10_audio.states hppr10_audio.jpg
FP 0 [Soulat12] fp0.pi0 5 7 10 63 62 33 12 0.283s fp0.log fp0.states fp0.jpg
AM02 [AM02] am02.pi0 3 3 4 53 70 11 5 0.091s am02.log am02.states am02.jpg
fp2 [Soulat12] fp2.pi0 5 7 10 208 228 43 12 3.18s fp2.log fp2.states fp2.jpg
LA02 2x5 [LA02] LA02_2.pi0 3 3 5 383 533 23 11 15s LA02_2.log LA02_2.states LA02_2.jpg
Case study Reference V0 |A| |X| |P| t Log Cartography
BB04 [BB04] bb.v0 5 7 10 66s bb.log bb.png

Description of the Case Studies

We can group our case studies in five classes.

  1. The FPs and EDFs case studies are composed of three cyclic tasks that need to be performed on a single machine. Therefore, the machine has to choose which task is active when several tasks are requiring computation. This is done in two ways, either with a Fixed Priority (FP) scheduler or an Earliest Deadline First scheduler (EDF). These case studies are being studied in the framework of the joint project Roscov between LSV and an industrial partner [Soulat12].
    For every FP scheduling example, each task tau_i has the following parameters: an offset O_i, a Wost Case Execution Time (WCET) C_i, a period T_i and a deadline to achieve a given goal (modeled by an extra automaton).
    For every EDF scheduling example, each task tau_i has the following parameters: an offset O_i, a WCET C_i, a period T_i, a deadline D_i to achieve each task, and a deadline to achieve a given goal (modeled by an extra automaton).
  2. The Task Chain case study does not use cyclic tasks but instead has a 4 task chain and a concurrent 3 task chain. Each task in a chain cannot start until the previous one has not terminated. Each task in each chain has a given fixed priority. A scheduler assigns which task has the computational time with a FP policy.
  3. CPR08 and LPPRC10 are two-cyclic-tasks problems with an EDF scheduler.
  4. AM02, LA02 2*5, LA02 3*5 case studies are problems of preemptive job-shop scheduling. AM02 is an example with two jobs on three machines; LA02 2*5 (resp. LA02 3*5) corresponds to the example from [LA02] (with 10 jobs on 5 machines) with here only the 2 (resp. 3) first jobs on 5 machines.
  5. BB04 case study corresponds to a three task example from [BB04, Section III, table 1]. It is an FP scheduling problem with three cyclic tasks on one machine. This case study actually uses the behavioral cartography algorithm (see [AF10]), hence we present it below.

Algorithms used

All of these case studies use the merging technique introduced in [AFS13atva].

For all case studies except three, the standard Inverse Method algorithm was used. To execute IMITATOR, use:

	> IMITATOR case_study.imi case_study.pi0 -with-merging -with-dot -with-log

Note that the CPR08 case study is analyzed using a partial exploration of depth 30. Hence, the command is:

	> IMITATOR case_study.imi case_study.pi0 -with-merging -with-dot -with-log -depth-limit 30

For the LA02 2*5 and LA02 3*5 case studies, we made use of Algorithm IMincl (introduced in [AS11]). To execute IMITATOR, use:

	> IMITATOR case_study.imi case_study.pi0 -merge -inclusion

For the BB04 case study, the cartography algorithm (introduced in [AF10], and iteratively calling the inverse method) was used. To execute IMITATOR, use:

	> IMITATOR bb.imi bb.v0 -merge -mode cover [-no-dot -no-log]

Full details about models and results are available in [Soulat12].

References

[ACEF09]
Étienne André, Thomas Chatain, Emmanuelle Encrenaz and Laurent Fribourg. An Inverse Method for Parametric Timed Automata. International Journal of Foundations of Computer Science 20(5), pages 819–836, 2009. (English) [PDF (published version) | PDF (author version) | BibTeX]
[AF10]
Étienne André and Laurent Fribourg. Behavioral Cartography of Timed Automata. In Antonín Kučera and Igor Potapov (eds.), RP’10, LNCS 6227, Springer, pages 76–90, September 2010. (English) [PDF (published version) | PDF (author version) | BibTeX | Slides]
[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]
[AFS13atva]
Étienne André, Laurent Fribourg and Romain Soulat. Merge and Conquer: State Merging in Parametric Timed Automata. In Hung Dang-Van and Mizuhito Ogawa (eds.), ATVA’13, LNCS 8172, Springer, pages 381–396, October 2013. [PDF (author version) | PDF (long author version) | BibTeX | Slides]
[AM02]
Yasmina Abdeddaïm and Oded Maler. Preemptive job-shop scheduling using stopwatch automata. In TACAS’02, pages 113–126, 2002.
[AS11]
Étienne André and Romain Soulat. Synthesis of Timing Parameters Satisfying Safety Properties. In Giorgio Delzanno and Igor Potapov (eds.), RP’11, LNCS 6945, Springer, pages 31–44, 2011. (English) [PDF (author version) | PDF (long author version) | BibTeX]
[BB04]
Enrico Bini and Giorgio C. Buttazzo. Schedulability analysis of periodic fixed priority systems. IEEE Trans. Computers, 53(11):1462–1473, 2004.
[CPR08]
Cimatti, Palopoli and Ramadian. Symbolic Computation of Schedulability Regions Using Parametric Timed Automata. In RTSS’08.
[LA02]
http://bach.istc.kobe-u.ac.jp/csp2sat/jss/
[LPPRC10]
Thi Thieu Hoa Le, Luigi Palopoli, Roberto Passerone, Yusi Ramadian, Alessandro Cimatti. Parametric Analysis of Distributed Firm Real-Time Systems: A Case Study. In ETFA’2010: 1-8.
[SGL97]
Jun Sun, Mark K. Gardner, and Jane W. S. Liu. Bounding Completion Times of Jobs with Arbitrary Release Times, Variable Execution Times, and Resource Sharing. IEEE Trans. Softw. Eng., 1997.
[Soulat12]
Romain Soulat. Scheduling with IMITATOR: Some Case Studies. Research Report, Laboratoire Spécification et Vérification, March 2012.

Contact

Étienne André