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].

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] |

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 |

We can group our case studies in five classes.

- 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). - 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. **CPR08**and**LPPRC10**are two-cyclic-tasks problems with an EDF scheduler.**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.**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.

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].

- [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.