IMITATOR

IMITATOR: Experiments Data for NFM 2015

Case Studies Related to the PRP Algorithm for Parametric Timed Automata

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

IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR 2.6.2 (build 845).

Download

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

Case studies

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]

Description of the Case Studies

A1

A1 is a sampled PTA proposed in [JLR13].

Sched1

This is a parametric scheduling problem studied in [LSAF14].

Sched2

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

Sched5

This is the model of the schedulability of 5 fixed-priority tasks in a single processor.

SPSMALL

This is a PTA model of an abstraction of the "SPSMALL" memory circuit commercialized by ST-Microelectronics [CEFX09].

Algorithms used

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

References

[ALNS15]
Étienne André, Giuseppe Lipari, Nguyễn Hoàng Gia and Sun Youcheng. Reachability Preservation Based Parameter Synthesis for Timed Automata. In Klaus Havelund, Gerard Holzmann, Rajeev Joshi (eds.), NFM’15, LNCS 9058, Springer, pages 50–65, April 2015. (English) [PDF | PDF (author version) | BibTeX | Slides]
[AS13]
Étienne André and Romain Soulat. The Inverse Method. ISTE Ltd and John Wiley & Sons Inc. ISBN: 9781848214477. January 2013. (English) [PDF | BibTeX]
[BFSV04]
Giacomo Bucci, Andrea Fedeli, Luigi Sassoli, and Enrico Vicario. Timed state space analysis of real-time preemptive systems. Transactions on Software Engineering, 30(2):97–111, 2004.
[CEFX09]
Rémy Chevallier, Emmanuelle Encrenaz-Tiphène, Laurent Fribourg, and Weiwen Xu. Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design, 34(1):59–81, 2009.
[JLR13]
Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for timed automata. In TACAS, volume 7795 of Lecture Notes in Computer Science, pages 401–415. Springer, 2013.
[LSAF14]
Giuseppe Lipari, Sun Youcheng, Étienne André and Laurent Fribourg. Toward Parametric Timed Interfaces for Real-Time Components. In Étienne André and Goran Frehse (eds.), SynCoP’14, EPTCS, April 2014.

Contact

Étienne André