IMITATOR: distributed case studies

• Home
• Download
• Case studies
• References
• Contact
• Links

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

• Source
• Binary (Ubuntu-like, Debian-like 64 bits)

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
3	random10	62	64.40 s	96.12 %	96.97 %/0.86	1.46 s
4	random10	80	57.12 s	97.74 %	97.18 %/0.40	1.56 s
5	random10	80	44.94 s	97.97 %	97.31 %/0.68	1.59 s
6	random10	96	43.50 s	97.79 %	97.33 %/0.82	1.74 s
7	random10	116	43.45 s	97.72 %	97.50 %/0.24	1.64 s
8	random10	114	38.47 s	97.75 %	97.62 %/0.30	1.59 s
9	random10	107	32.35 s	97.79 %	97.40 %/1.34	1.93 s
10	random10	142	37.94 s	97.72 %	97.53 %/0.23	1.97 s
12	random10	135	30.92 s	97.72 %	97.47 %/0.36	2.17 s
14	random10	153	28.06 s	97.71 %	97.06 %/0.95	2.38 s
16	random10	170	27.15 s	97.77 %	96.55 %/1.85	2.41 s
18	random10	149	22.48 s	97.63 %	95.75 %/2.57	2.25 s
20	random10	171	23.17 s	97.76 %	96.66 %/1.63	2.40 s
22	random10	206	25.21 s	97.23 %	94.89 %/3.50	2.63 s
24	random10	213	23.98 s	97.72 %	96.57 %/1.31	2.49 s
2	random20	49	100.73 s	96.93 %	96.93 %/0	1.29 s
3	random20	61	63.30 s	96.97 %	97.14 %/0.17	1.21 s
4	random20	66	47.04 s	96.90 %	97.20 %/0.49	1.35 s
5	random20	78	42.33 s	97.70 %	97.34 %/0.40	1.28 s
6	random20	88	40.89 s	96.50 %	97.33 %/0.71	1.68 s
7	random20	98	39.50 s	96.72 %	97.38 %/0.46	1.76 s
8	random20	95	32.74 s	97.81 %	97.51 %/0.37	1.54 s
9	random20	102	31.46 s	97.77 %	97.55 %/0.32	1.61 s
10	random20	105	29.31 s	97.47 %	97.51 %/0.30	1.63 s
18	random20	163	23.98 s	97.74 %	97.15 %/0.86	2.29 s
20	random20	169	22.16 s	97.87 %	96.20 %/2.16	2.31 s
22	random20	141	18.30 s	97.66 %	94.12 %/4.44	2.40 s
24	random20	185	21.40 s	97.96 %	93.97 %/4.04	2.58 s

Sched3

NP	Selection	Constraints	Total time	Master wait.	W.\ occ. (mean/std dev)	Next point time
2	seq	59	39.51 s	98.47 %	98.5 %/0	0.05 s
3	seq	62	22.26 s	98.47 %	98.5 %/0.04	0.05 s
4	seq	69	16.96 s	98.47 %	98.5 %/0.05	0.05 s
5	seq	77	14.12 s	98.38 %	98.4 %/ 0.08	0.06 s
6	seq	85	13.12 s	98.48 %	98.4 %/0.09	0.07 s
7	seq	93	12.04 s	98.45 %	98.4 %/0.07	0.08 s
8	seq	98	11.29 s	98.46 %	98.5 %/0.09	0.08 s
9	seq	103	10.49 s	98.53 %	98.4 %/0.08	0.09 s
10	seq	107	9.85 s	98.45 %	98.3 %/0.08	0.10 s
12	seq	113	8.74 s	98.29 %	98.3 %/0.17	0.10 s
14	seq	126	8.14 s	98.23 %	98.2 %/0.20	0.12 s
16	seq	130	7.23 s	98.08 %	98.1 %/0.19	0.13 s
18	seq	142	7.00 s	97.73 %	97.7 %/0.37	0.13 s
20	seq	153	6.84 s	97.41 %	97.7 %/0.40	0.15 s
22	seq	158	6.47 s	98.02 %	98.1 %/0.25	0.14 s
24	seq	163	6.26 s	98.47 %	98.1 %/0.36	0.15 s
2	random10	60	40.47 s	98.54 %	98.54 %/0	0.03 s
3	random10	64	22.93 s	98.63 %	98.60 %/0.03	0.03 s
4	random10	71	16.70 s	98.41 %	98.44 %/0.03	0.04 s
5	random10	77	14.19 s	98.50 %	98.51 %/0.02	0.04 s
6	random10	75	11.62 s	98.52 %	98.52 %/0.03	0.05 s
7	random10	82	10.65 s	98.59 %	98.51 %/0.09	0.05 s
8	random10	81	9.38 s	98.54 %	98.53 %/0.06	0.06 s
9	random10	76	7.67 s	98.30 %	98.42 %/0.11	0.04 s
10	random10	93	8.47 s	98.45 %	98.42 %/0.09	0.07 s
12	random10	90	6.92 s	98.53 %	98.48 %/0.08	0.06 s
14	random10	83	5.27 s	97.76 %	97.91 %/0.20	0.05 s
16	random10	89	4.91 s	96.80 %	97.48 %/0.58	0.07 s
18	random10	104	5.23 s	98.01 %	97.81 %/0.30	0.08 s
20	random10	114	5.09 s	97.47 %	98.23 %/0.39	0.06 s
22	random10	96	4.09 s	98.15 %	97.79 %/0.52	0.09 s
24	random10	104	4.25 s	97.23 %	98.03 %/0.55	0.08 s
2	random20	60	41.04 s	98.56 %	98.56 %/0	0.04 s
3	random20	65	22.18 s	98.47 %	98.45 %/0.02	0.04 s
4	random20	66	15.45 s	98.45 %	98.40 %/0.04	0.04 s
5	random20	70	12.68 s	98.32 %	98.47 %/0.09	0.05 s
6	random20	76	11.49 s	98.52 %	98.47 %/0.05	0.05 s
7	random20	76	9.83 s	98.53 %	98.46 %/0.11	0.07 s
8	random20	75	8.44 s	98.52 %	98.44 %/0.08	0.06 s
9	random20	82	8.25 s	98.43 %	98.48 %/0.08	0.08 s
10	random20	80	7.29 s	98.42 %	98.48 %/0.08	0.06 s
12	random20	89	6.87 s	98.53 %	98.39 %/0.19	0.08 s
14	random20	88	5.64 s	98.43 %	98.22 %/0.17	0.07 s
16	random20	86	4.91 s	98.14 %	97.98 %/0.21	0.07 s
18	random20	99	5.04 s	96.87 %	97.77 %/0.42	0.11 s
20	random20	100	4.65 s	97.67 %	97.57 %/0.64	0.09 s
22	random20	98	4.23 s	98.64 %	97.87 %/0.63	0.07 s
24	random20	106	4.24 s	98.2 %7	97.72 %/0.69	0.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).