This page is dedicated to the case studies related to the manuscript Reachability Preservation Based Parameter Synthesis for Timed Automata by Étienne André, Giuseppe Lipari, Nguyễn Hoàng Gia and Sun Youcheng, published in the proceedings of the NFM’15 [ALNS15].
The version of IMITATOR used to run the experiments is IMITATOR 2.6.2 (build 845).
[edit (2016/08/13)] The above archive seems to not contain all files necessary for compiling.
The full source code of the version used for these experiments can be downloaded on Github: SHA hash d327b4c.
In addition, for legacy purpose, the non-distributed version (that cannot be used to reproduce these distributed experiments, but that comes with no dependencies), can be found here for Linux 64 bits (recompiled on 2018/03/28).
We present in the following table a list of case studies computed using various algorithms using IMITATOR.
The model can be obtained by clicking on the case study name; the rectangular parameter domain can be obtained by clicking on the number of integer points (|V| column); logs including results can be obtained by clicking on the response time of each algorithm; a graphical representation can be obtained by clicking on the [g] (when available).
To lift discrepancies between different executions (due to possible load variations on the cluster), we run each experiment twice. The upper execution time is the average (as taken into account in the paper), and the lower, small execution times are each of the two executions.
| Case study | Ref | |X| | |P| | |V| | EF | BC | PRPC | PRPC distr |
|---|---|---|---|---|---|---|---|---|
| A1 | [JLR13] | 2 | 2 | 2601 | 0.0665 s 0.06 s [g] | 0.073 s [g] |
T.O. | 0.078 s 0.077 s [g] | 0.079 s [g] |
0.05045 s 0.05 s [g] | 0.0509 s [g] |
| Sched1 | [LSAF14] | 13 | 2 | 6561 | T.O. | T.O. | 1594.5 s 1619 s [g] | 1570 s [g] |
218.5 s 207 s [g] | 230 s [g] |
| Sched2.50.0 | [BFSV04] | 6 | 2 | 3321 | 9.25 s 8.81 s [g] | 9.69 s [g] |
990 s 1043 s [g] | 937 s [g] |
14.5 s 13.7 s [g] | 15.3 s [g] |
4.085 s 4.73 s [g] | 3.44 s [g] |
| Sched2.50.2 | [BFSV04] | 6 | 2 | 3321 | 662.5 s 643 s [g] | 682 s [g] |
T.O. | 213 s 232 s [g] | 194 s [g] |
84.05 s 81.9 s [g] | 86.2 s [g] |
| Sched2.100.0 | [BFSV04] | 6 | 2 | 972971 | 21.4 s 20.8 s [g] | 22 s [g] |
2092.5 s 2300 s [g] | 1885 s [g] |
116 s 109 s [g] | 123 s [g] |
10.085 s 9.37 s [g] | 10.8 s [g] |
| Sched2.100.2 | [BFSV04] | 6 | 2 | 972971 | 3756.5 s 3677 s [g] | 3836 s [g] |
T.O. | 4556.5 s 4540 s [g] | 4573 s [g] |
1543 s 1256 s [g] | 1830 s [g] |
| Sched5 | [LSAF14] | 21 | 2 | 1681 | 352 s 364 s [g] | 340 s [g] |
T.O. | T.O. | 917 s 895 s | 939 s |
| SPSMALL | [CEFX09] | 11 | 2 | 3082 | 7.49 s 8 s [g] | 6.98 s [g] |
587 s 624 s [g] | 550 s [g] |
117.5 s 129 s [g] | 106 s [g] |
11.2 s 11.1 s [g] | 11.3 s [g] |
A1 is a sampled PTA proposed in [JLR13].
This is a parametric scheduling problem studied in [LSAF14].
These are several variants (using the size of the bounded parameter domain, the value of the jitter and the value of parameter a) of a parametric scheduling problem studied in [BFSV04] and [JLR13].
This is the model of the schedulability of 5 fixed-priority tasks in a single processor.
This is a PTA model of an abstraction of the "SPSMALL" memory circuit commercialized by ST-Microelectronics [CEFX09].
For all case studies except A1, the following commands were used:
> IMITATOR case_study.imi case_study.v0 -mode EF -merge -output-cart
> IMITATOR case_study.imi case_study.v0 -mode cover -merge -output-cart
> IMITATOR case_study.imi case_study.v0 -mode cover -EFIM -merge -output-cart
> mpiexec -n 12 IMITATOR case_study.imi case_study.v0 -mode cover -EFIM -distributed subpart -merge -output-cart
For A1, add:
-depth-limit 10
