This page is dedicated to the case studies related to the paper Dynamic Clock Elimination in Parametric Timed Automata.

The version of IMITATOR used to compute the case studies is **IMITATOR 2.6.1**.

It can be downloaded from the download page.

We present in the following table a list of case studies computed using the inverse method using the above implementation of IMITATOR.

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, and for each of the 2 algorithms, the number |S| of states computed, the number |T| of transitions computed, the computation time t in seconds (excluding the generation of the graphical outputs), and whether the result is complete or maybe not complete. In the last 2 columns, we compare the results: first, we divide the number of states in IM by the number of states in IMdyn and multiply by 100 (hence, a number smaller than 100 denotes an improvement of IMdyn); second, we perform the same comparison for the computation time.

Experiments were performed on a KUbuntu 13.04 64 bits system running on an Intel Core i7 CPU 2.67GHz with 4 GiB of RAM.

Case study | Reference | Pi0 | |X| | |P| | IM | IMdyn | Comparison | |||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

|S| | |T| | t | Complete | Result | |S| | |T| | t | Complete | Result | States | time | |||||

Figure 2 | [Andre13] | loopingDynamic.pi0 | 2 | 2 | - | - | Loop | - | - | 2 | 2 | 0.007 s | Yes | log – states – trace set | 0 | 0 |

Figure 3 | [Andre13] | exClockElimination.pi0 | 2 | 2 | - | - | Loop | - | - | 6 | 8 | 0.006 s | Yes | log – states – trace set | 0 | 0 |

And-Or | [CC05] | AndOr.pi0 | 4 | 12 | 11 | 11 | 0.047 s | Yes | log – states – traces | 11 | 11 | 0.05 s | Yes | log – states – trace set | 100 | 106 |

SPSMALL memory | [AS13] | spsmall.pi0 | 10 | 26 | 31 | 30 | 0.58 s | Yes | log – states – traces | 31 | 30 | 0.584 s | Yes | log – states – trace set | 100 | 101 |

Train | [AHV93] | TrainAHV93.pi0 | 3 | 6 | 78 | 94 | 0.1 s | Yes | log – states – traces | 61 | 76 | 0.072 s | Yes | log – states – trace set | 78 | 72 |

BRP | [DKRT97] | brp.pi0 | 7 | 6 | 429 | 474 | 3.5 s | Yes | log – states – traces | 426 | 473 | 3.21 s | Yes | log – states – trace set | 99 | 92 |

CSMA/CD bc6 | [KNSW07] | csmacdPrism6.pi0 | 3 | 3 | 13365 | 14271 | 19.6 s | Yes | log – states – traces | 13365 | 14271 | 19.5 s | Yes | log – states – trace set | 100 | 99 |

RCP | [HRSV02] | RCP.pi0 | 5 | 6 | 327 | 518 | 0.68 s | Yes | log – states – traces | 181 | 282 | 0.41 s | Yes | log – states – trace set | 55 | 60 |

AAM06 | [AAM06] | maler_2_4.pi0 | 3 | 8 | 1497 | 1844 | 8.28 s | Yes | log – states – traces | 768 | 997 | 2.92 s | Yes | log – states – trace set | 51 | 35 |

AM02 | [AM02] | am02.pi0 | 3 | 4 | 182 | 215 | 0.392 s | Yes | log – states – traces | 182 | 215 | 0.386 s | Yes | log – states – trace set | 100 | 98 |

BB04 | [BB04] | bb.pi0 | 6 | 7 | 806 | 827 | 25.4 s | ? | log – states – traces | 806 | 827 | 27.2 s | ? | log – states – trace set | 100 | 107 |

CTC | [???] | concurent_tasks_chain.pi0 | 15 | 21 | 1364 | 1363 | 83.4 s | Yes | log – states – traces | 201 | 291 | 2.52 s | Yes | log – states – trace set | 15 | 3 |

LA02 | [Tamura07] | LA02_2.pi0 | 3 | 5 | 6290 | 8023 | 710 s | ? | log – states – traces | 4932 | 7154 | 473 s | ? | log – states – trace set | 78 | 67 |

LPPRC10 | [LPPRC10] | hppr10_audio.pi0 | 4 | 7 | 78 | 102 | 0.375 s | ? | log – states – traces | 78 | 102 | 0.395 s | ? | log – states – trace set | 100 | 105 |

These 2 examples are presented in [Andre13].

The AndOr case study consists in an "AND" gate linked to an "OR" gate in a cyclic manner.

The SPSMALL case study is the model of an abstraction of an asynchronous circuit designed and sold by ST-Microelectronics.

This case study is classical train-gate-controller.

BRP is the bounded retransmission protocol.

The CSMA/CD model corresponds to the non-probabilistic version of the model described in [KNSW07] with a maximum backoff of 6.

RCP is the root contention protocol of the IEEE 1394 (“FireWire”) High Performance Serial Bus, considered in the parametric framework in [HRSV02].

The AAM06 case study is a problem of non-preemptive scheduling. Two sequences of tasks have to run concurrently trough 4 machines. The goal is to schedule the tasks to meet the deadline on the overall execution time.

The AM02 case study is a problem of preemptive job-shop scheduling with two jobs on three machines.

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

The CTC (concurrent 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.

The **LPPRC10** is a two-cyclic-tasks problem with an EDF scheduler.

For all case studies, the standard inverse method IM was called using the following options:

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

For all case studies, the inverse method with dynamic clock elimination IMdyn was called using the following options:

> IMITATOR case_study.imi case_study.pi0 -dynamic-elimination -with-dot -with-log

- [AAM06]
- Yasmina Abdeddaïm, Eugene Asarin, and Oded Maler.
*Scheduling with timed automata*. In Theoretical Computer Science 354(2), pages 272–300, 2006. - [AM02]
- Yasmina Abdeddaïm and Oded Maler.
*Preemptive job-shop scheduling using stopwatch automata*. In TACAS'02, pages 113–126, 2002. - [Andre13]
- Étienne André.
*Dynamic Clock Elimination in Parametric Timed Automata*. In FSFMA’13, OASIcs (volume 31), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, pages 18–31, July 2013. - [AS13]
- Étienne André and Romain Soulat. The Inverse Method. ISTE Ltd and John Wiley & Sons Inc., 2013.
- [BB04]
- Enrico Bini and Giorgio C. Buttazzo.
*Schedulability analysis of periodic fixed priority systems*. IEEE Trans. Computers, 53(11):1462–1473, 2004. - [CC05]
- Robert Clarisó, Jordi Cortadella.
*Verification of Concurrent Systems with Parametric Delays Using Octahedra*. In ACSD’05, 2005. - [DKRT97]
- P.R. D’Argenio, J.P. Katoen, T.C. Ruys, and G.J. Tretmans.
*The bounded retransmission protocol must be on time!*. In TACAS’97. - [HRSV02]
- T.S. Hune, J.M.T. Romijn, M.I.A. Stoelinga, and F.W. Vaandrager.
*Linear parametric model checking of timed automata*. Journal of Logic and Algebraic Programming, 2002. - [KNSW07]
- M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang.
*Symbolic model checking for probabilistic timed automata*. Information and Computation, 205(7):1027–1077, 2007. - [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. - [Tamura07]
- Naoyuki Tamura. CSP2SAT: JSS benchmark results. 2007.