IMITATOR

IMITATOR: Experiments Data for ICFEM 2015

Case Studies Related to the Tool Paper on the Enhanced Distributed Cartography (2015)

This page is dedicated to the case studies related to the manuscript Enhanced Distributed Behavioral Cartography of Parametric Timed Automata by Étienne André, Camille Coti and Nguyễn Hoàng Gia, published in the proceedings of ICFEM’15 [ACN15].

IMITATOR

The version of IMITATOR used to compute the case studies is IMITATOR 2.7-beta2 (build 1073).

Download

Unfortunately, we were not able to compile a standalone distributed binary. Hence you need to compile from sources to run distributed experiments (cf. the installation instructions for IMITATOR).

Case studies

We present in the following the list of case studies used for our experiments.

Case study Flip-Flop4

Model

Modelflipflop4D.imi
Reference[CC07]
Model (graphic)flipflop4D-pta.jpg
Domainflipflop4D.v0

Command to execute IMITATOR

Monolithic version

> imitator flipflop4D.imi flipflop4D.v0 -mode cover -output-result -output-cart

Distributed version (replace {DISTRIBUTIONMODE} with the actual distribution algorithm)

> imitator flipflop4D.imi flipflop4D.v0 -mode cover -distributed {DISTRIBUTIONMODE} -verbose mute -output-result -output-cart

Results

Algorithm1 4 8 16 32 64 128
Static 1 4 8 16 32 64 128
Sequential 1 4 8 16 32 64 128
Random 1 4 8 16 32 64 128
Shuffle 1 4 8 16 32 64 128
Subpart 1 4 8 16 32 64 128
Subpart+H 1 4 8 16 32 64 128

Plots

Execution time for Flip-Flop4 Speedup for Flip-Flop4

Case study Root Contention Protocol

Model

ModelRCP.imi
Reference[CS01]
Model (graphic)RCP-pta.jpg
DomainRCP.v0

Command to execute IMITATOR

Monolithic version

> imitator RCP.imi RCP.v0 -mode cover -output-result -output-cart

Distributed version (replace {DISTRIBUTIONMODE} with the actual distribution algorithm)

> imitator RCP.imi RCP.v0 -mode cover -distributed {DISTRIBUTIONMODE} -verbose mute -output-result -output-cart

Results

Algorithm1 4 8 16 32 64 128
Static 1 4 8 16 32 64 128
Sequential 1 4 8 16 32 64 128
Random 1 4 8 16 32 64 128
Shuffle 1 4 8 16 32 64 128
Subpart 1 4 8 16 32 64 128
Subpart+H 1 4 8 16 32 64 128

Plots

Execution time for Root Contention Protocol Speedup for Root Contention Protocol

Case study Sched3-2

Model

Modelsched3-2.imi
Reference[LSAF14]
Model (graphic)sched3-2-pta.jpg
Domainsched3-2.v0

Command to execute IMITATOR

Monolithic version

> imitator sched3-2.imi sched3-2.v0 -mode cover -output-result -output-cart

Distributed version (replace {DISTRIBUTIONMODE} with the actual distribution algorithm)

> imitator sched3-2.imi sched3-2.v0 -mode cover -distributed {DISTRIBUTIONMODE} -verbose mute -output-result -output-cart

Results

Algorithm1 4 8 16 32 64 128
Static 1 4 8 16 32 64 128
Sequential 1 4 8 16 32 64 128
Random 1 4 8 16 32 64 128
Shuffle 1 4 8 16 32 64 128
Subpart 1 4 8 16 32 64 128
Subpart+H 1 4 8 16 32 64 128

Plots

Execution time for Sched3-2 Speedup for Sched3-2

Case study Sched3B-2

Model

Modelsched3B-2.imi
Reference[LSAF14]
Model (graphic)sched3B-2-pta.jpg
Domainsched3B-2.v0

Command to execute IMITATOR

Monolithic version

> imitator sched3B-2.imi sched3B-2.v0 -mode cover -output-result -output-cart

Distributed version (replace {DISTRIBUTIONMODE} with the actual distribution algorithm)

> imitator sched3B-2.imi sched3B-2.v0 -mode cover -distributed {DISTRIBUTIONMODE} -verbose mute -output-result -output-cart

Results

Algorithm1 4 8 16 32 64 128
Static 1 4 8 16 32 64 128
Sequential 1 4 8 16 32 64 128
Random 1 4 8 16 32 64 128
Shuffle 1 4 8 16 32 64 128
Subpart 1 4 8 16 32 64 128
Subpart+H 1 4 8 16 32 64 128

Plots

Execution time for Sched3B-2 Speedup for Sched3B-2

Case study Sched3B-3

Model

Modelsched3B-3.imi
Reference[LSAF14]
Model (graphic)sched3B-3-pta.jpg
Domainsched3B-3.v0

Command to execute IMITATOR

Monolithic version

> imitator sched3B-3.imi sched3B-3.v0 -mode cover -output-result -output-cart

Distributed version (replace {DISTRIBUTIONMODE} with the actual distribution algorithm)

> imitator sched3B-3.imi sched3B-3.v0 -mode cover -distributed {DISTRIBUTIONMODE} -verbose mute -output-result -output-cart

Results

Algorithm1 4 8 16 32 64 128
Static 1 4 8 16 32 64 128
Sequential 1 4 8 16 32 64 128
Random 1 4 8 16 32 64 128
Shuffle 1 4 8 16 32 64 128
Subpart 1 4 8 16 32 64 128
Subpart+H 1 4 8 16 32 64 128

Plots

Execution time for Sched3B-3 Speedup for Sched3B-3

Case study Sched5

Model

Modelsched5.imi
Reference[LSAF14]
Model (graphic)sched5-pta.jpg
Domainsched5.v0

Command to execute IMITATOR

Monolithic version

> imitator sched5.imi sched5.v0 -mode cover -output-result -output-cart

Distributed version (replace {DISTRIBUTIONMODE} with the actual distribution algorithm)

> imitator sched5.imi sched5.v0 -mode cover -distributed {DISTRIBUTIONMODE} -verbose mute -output-result -output-cart

Results

Algorithm1 4 8 16 32 64 128
Static 1 4 8 16 32 64 128
Sequential 1 4 8 16 32 64 128
Random 1 4 8 16 32 64 128
Shuffle 1 4 8 16 32 64 128
Subpart 1 4 8 16 32 64 128
Subpart+H 1 4 8 16 32 64 128

Plots

Execution time for Sched5 Speedup for Sched5

Case study SiMoP

Model

Modelsimop.imi
Reference[ACDFR09]
Model (graphic)simop-pta.jpg
Domainsimop.v0

Command to execute IMITATOR

Monolithic version

> imitator simop.imi simop.v0 -merge -mode cover -output-result -output-cart

Distributed version (replace {DISTRIBUTIONMODE} with the actual distribution algorithm)

> imitator simop.imi simop.v0 -merge -mode cover -distributed {DISTRIBUTIONMODE} -verbose mute -output-result -output-cart

Results

Algorithm1 4 8 16 32 64 128
Static 1 4 8 16 32 64 128
Sequential 1 4 8 16 32 64 128
Random 1 4 8 16 32 64 128
Shuffle 1 4 8 16 32 64 128
Subpart 1 4 8 16 32 64 128
Subpart+H 1 4 8 16 32 64 128

Plots

Execution time for SiMoP Speedup for SiMoP

References

[ACDFR09]
Étienne André, Thomas Chatain, Olivier De Smet, Laurent Fribourg and Silvain Ruel. Synthèse de contraintes temporisées pour une architecture d’automatisation en réseau. In Didier Lime and Olivier H. Roux (eds.), MSR’09, Journal Européen des Systèmes Automatisés 43(7-9), Hermès, pages 1049–1064, 2009.
[ACN15]
Étienne André, Camille Coti and Nguyễn Hoàng Gia. Enhanced Distributed Behavioral Cartography of Parametric Timed Automata. In Michael Butler, Sylvain Conchon and Fatiha Zaïdi (eds.), ICFEM’15, Springer LNCS 9407, pages 319–335, November 2015. [PDF | PDF (author version) | Slides]
[CC07]
Robert Clarisó, Jordi Cortadella. The Octahedron Abstract Domain. In Science of Computer Programming 64(1), pages 115-139, 2007.
[CS01]
Aurore Collomb-Annichini and Mihaela Sighireanu. Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. In Proceedings of the Real-Time Tools Workshop (RT-TOOLS’2001).
[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é