IMITATOR

IMITATOR: distributed case studies

Case Studies Related to the Distributed Behavioral Cartography of Timed Automata

This page is dedicated to the case studies related to the submitted manuscript Distributed Behavioral Cartography of Timed Automata.

Parallel IMITATOR ("PaTATOR")

The new distributed version of IMITATOR used to compute the case studies is IMITATOR 2.6.2.

Download

Case studies

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

Case study |P| |X| |D| Tiles
SIMOP 2 8 10 201 48
Sched3 2 13 286 59

Description of the Case Studies

SIMOP

SIMOP is a networked automation system studied in, e.g., [Andre10].

Scheduling

Sched3 is a distributed real-time system with preemption studied in [LSAF14].

Algorithms used

For all case studies, the standard behavioral cartography was called using the following options:

	> IMITATOR case_study.imi case_study.v0 -mode cover -merge -no-random

For the sequential distributed algorithm, add:

	> -distributed sequential

For the random algorithm, add (where XXXX is the maximum number of failed attempts before switching to the sequential algorithm):

	> -distributed randomXXXX

Experiments

Simop

NP Selection Constraints Total time Master wait. W.\ occ. (mean/std dev) Next point time
2 seq 48 97.75 s 96.68 % 96.68 %/0 1.38 s
3 seq 80 86.51 s 96.68 % 96.89 %/0.21 2.24 s
4 seq 107 75.38 s 97.28 % 96.72 %/0.45 3.08 s
5 seq 132 72.30 s 97.37 % 96.86 %/0.31 3.70 s
6 seq 152 68.79 s 97.11 % 96.80 %/0.35 4.29 s
7 seq 178 67.39 s 97.27 % 96.86 %/0.58 5.06 s
8 seq 195 65.35 s 97.10 % 96.84 %/0.49 5.68 s
9 seq 209 62.16 s 97.29 % 96.86 %/0.51 6.04 s
10 seq 224 60.70 s 96.50 % 96.96 %/0.52 6.28 s
12 seq 244 55.09 s 96.99 % 96.90 %/0.62 6.99 s
14 seq 269 50.01 s 97.01 % 96.28 %/1.91 7.81 s
16 seq 281 45.24 s 96.99 % 96.30 %/1.16 7.51 s
18 seq 297 43.20 s 97.33 % 95.99 %/1.64 7.77 s
20 seq 313 41.45 s 97.14 % 95.40 %/1.99 8.35 s
22 seq 325 40.39 s 96.84 % 94.98 %/2.39 8.19 s
24 seq 342 40.43 s 97.26 % 93.45 %/4.42 9.01 s
3random106264.40 s96.12 %96.97 %/0.861.46 s
4random108057.12 s97.74 %97.18 %/0.401.56 s
5random108044.94 s97.97 %97.31 %/0.681.59 s
6random109643.50 s97.79 %97.33 %/0.821.74 s
7random1011643.45 s97.72 %97.50 %/0.241.64 s
8random1011438.47 s97.75 %97.62 %/0.301.59 s
9random1010732.35 s97.79 %97.40 %/1.341.93 s
10random1014237.94 s97.72 %97.53 %/0.231.97 s
12random1013530.92 s97.72 %97.47 %/0.362.17 s
14random1015328.06 s97.71 %97.06 %/0.952.38 s
16random1017027.15 s97.77 %96.55 %/1.852.41 s
18random1014922.48 s97.63 %95.75 %/2.572.25 s
20random1017123.17 s97.76 %96.66 %/1.632.40 s
22random1020625.21 s97.23 %94.89 %/3.502.63 s
24random1021323.98 s97.72 %96.57 %/1.312.49 s
2random2049100.73 s96.93 %96.93 %/01.29 s
3random206163.30 s96.97 %97.14 %/0.171.21 s
4random206647.04 s96.90 %97.20 %/0.491.35 s
5random207842.33 s97.70 %97.34 %/0.401.28 s
6random208840.89 s96.50 %97.33 %/0.711.68 s
7random209839.50 s96.72 %97.38 %/0.461.76 s
8random209532.74 s97.81 %97.51 %/0.371.54 s
9random2010231.46 s97.77 %97.55 %/0.321.61 s
10random2010529.31 s97.47 %97.51 %/0.301.63 s
18random2016323.98 s97.74 %97.15 %/0.862.29 s
20random2016922.16 s97.87 %96.20 %/2.162.31 s
22random2014118.30 s97.66 %94.12 %/4.442.40 s
24random2018521.40 s97.96 %93.97 %/4.042.58 s

Sched3

NP Selection Constraints Total time Master wait. W.\ occ. (mean/std dev) Next point time
2seq5939.51 s98.47 %98.5 %/00.05 s
3seq6222.26 s98.47 %98.5 %/0.040.05 s
4seq6916.96 s98.47 %98.5 %/0.050.05 s
5seq7714.12 s98.38 %98.4 %/ 0.080.06 s
6seq8513.12 s98.48 %98.4 %/0.090.07 s
7seq9312.04 s98.45 %98.4 %/0.070.08 s
8seq9811.29 s98.46 %98.5 %/0.090.08 s
9seq10310.49 s98.53 %98.4 %/0.080.09 s
10seq1079.85 s98.45 %98.3 %/0.080.10 s
12seq1138.74 s98.29 %98.3 %/0.170.10 s
14seq1268.14 s98.23 %98.2 %/0.200.12 s
16seq1307.23 s98.08 %98.1 %/0.190.13 s
18seq1427.00 s97.73 %97.7 %/0.370.13 s
20seq1536.84 s97.41 %97.7 %/0.400.15 s
22seq1586.47 s98.02 %98.1 %/0.250.14 s
24seq1636.26 s98.47 %98.1 %/0.360.15 s
2random106040.47 s98.54 %98.54 %/00.03 s
3random106422.93 s98.63 %98.60 %/0.030.03 s
4random107116.70 s98.41 %98.44 %/0.030.04 s
5random107714.19 s98.50 %98.51 %/0.020.04 s
6random107511.62 s98.52 %98.52 %/0.030.05 s
7random108210.65 s98.59 %98.51 %/0.090.05 s
8random10819.38 s98.54 %98.53 %/0.060.06 s
9random10767.67 s98.30 %98.42 %/0.110.04 s
10random10938.47 s98.45 %98.42 %/0.090.07 s
12random10906.92 s98.53 %98.48 %/0.080.06 s
14random10835.27 s97.76 %97.91 %/0.200.05 s
16random10894.91 s96.80 %97.48 %/0.580.07 s
18random101045.23 s98.01 %97.81 %/0.300.08 s
20random101145.09 s97.47 %98.23 %/0.390.06 s
22random10964.09 s98.15 %97.79 %/0.520.09 s
24random101044.25 s97.23 %98.03 %/0.550.08 s
2random206041.04 s98.56 %98.56 %/00.04 s
3random206522.18 s98.47 %98.45 %/0.020.04 s
4random206615.45 s98.45 %98.40 %/0.040.04 s
5random207012.68 s98.32 %98.47 %/0.090.05 s
6random207611.49 s98.52 %98.47 %/0.050.05 s
7random20769.83 s98.53 %98.46 %/0.110.07 s
8random20758.44 s98.52 %98.44 %/0.080.06 s
9random20828.25 s98.43 %98.48 %/0.080.08 s
10random20807.29 s98.42 %98.48 %/0.080.06 s
12random20896.87 s98.53 %98.39 %/0.190.08 s
14random20885.64 s98.43 %98.22 %/0.170.07 s
16random20864.91 s98.14 %97.98 %/0.210.07 s
18random20995.04 s96.87 %97.77 %/0.420.11 s
20random201004.65 s97.67 %97.57 %/0.640.09 s
22random20984.23 s98.64 %97.87 %/0.630.07 s
24random201064.24 s98.2 %797.72 %/0.690.08 s

References

[Andre10]
Étienne André. An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems. Ph.D. thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2010.
[AS13]
Étienne André and Romain Soulat. The Inverse Method. ISTE Ltd and John Wiley & Sons Inc., 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é

This page makes use of valid HTML 5 and valid CSS.

Content and CSS can be reused and modified under the terms of license Creative Commons Attribution 3.0 Unported (CC BY 3.0).

Creative Commons Attribution 3.0 Unported