IMITATOR: Experiments Data for ‘Distributed parametric model checking timed automata under non-Zenoness assumption’ (FMSD, 2022)

Case Studies Related to Distributed parametric model checking timed automata under non-Zenoness assumption

This page is dedicated to the case studies related to the manuscript Distributed parametric model checking timed automata under non-Zenoness assumption by Étienne André, Hoang Gia Nguyen, Laure Petrucci and Jun Sun.

IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR 2.9.1.

Download

Source code
Standalone binary for Linux (Ubuntu-like, Debian-like 64 bits)

Non-distributed case studies

We present in the following table a list of case studies computed using various algorithms using IMITATOR.

Benchmark						SynthCycle			CUBdetect + SynthNZ					CUBtrans + SynthNZ
Name	Ref	\|A\|	\|X\|	\|P\|	\|L\|	t (s)	Result	Approximation?	detection t (s)	Total t (s)	CUB for	Result	Approximation?	transformation t (s)	Total t (s)	\|L CUB\|	Result	Approximation?
CSMA/CD	[KNSW07]	3	3	3	28	timeout	true	possibly invalid	0.013	0.013	false	-	-	0.3	timeout	74	true	exact
Fischer	[AHV93]	3	2	4	13	timeout	true	possibly invalid	0.003	0.003	false	-	-	0.012	timeout	20	true	exact
RCP	[CS01]	5	6	5	48	timeout	some	possibly invalid	0.013	0.013	false	-	-	0.348	timeout	71	false	under-approximation
WFAS	[BBLS15]	3	4	2	10	timeout	some	possibly invalid	0.009	0.009	false	-	-	0.246	1848	40	some	exact
AndOr	[CC05]	4	4	4	27	timeout	some	possibly invalid	0.012	0.012	false	-	-	0.059	timeout	34	some	under-approximation
Flip-flop	[CC04]	5	5	2	52	0.058	false	exact	0.002	0.086	true	false	exact	0.01	0.972	58	false	exact
Sched5	[LSAF14]	12	21	2	153	190	false	exact	0.051	0.051	false	-	-	1.18	timeout	180	false	under-approximation
simop	[ACDFR09]	5	8	2	46	timeout	false	possibly invalid	0.012	0.012	false	-	-	0.219	timeout	81	false	under-approximation
train-gate		4	5	9	11	timeout	false	possibly invalid	0	timeout	some	false	under-approximation	0.059	timeout	23	false	under-approximation
coffee	[Andre18]	3	2	3	4	timeout	some	possibly invalid	0	timeout	some	some	under-approximation	0.012	timeout	10	some	under-approximation
CUBPTA1	[ANPS17]	3	1	3	2	0.006	true	over-approximation	0	0.015	some	some	under-approximation	0.006	0.073	6	some	exact
JLR15	[JLR15]	3	2	2	2	timeout	false	possibly invalid	0	timeout	true	false	under-approximation	0	timeout	3	false	under-approximation

Distributed case studies

Model								Single Node (CUBtrans)		Multi Node (DistCUBtrans)
Name	Ref	\|A\|	\|X\|	\|P\|	\|L\|	\|DCUB-PTA\|	\|CUB-PTA\|	t (s)	Approximation?	\|ESC\|	\|node\| limit	4 nodes t (s)	6 nodes t (s)	8 nodes t (s)	Approximation?
CSMA/CD	[KNSW07]	3	4	3	79	3	5	536.4	under-approximation	4	5	991.7 log	990.1 log	-	under-approximation
Fischer	[AHV93]	3	3	9	127	3	7	timeout	under-approximation	5	6	timeout res log	timeout res log	-	under-approximation
RCP	[CS01]	5	7	7	89	5	6	948.8	exact	2	3	915.7 res log	-	-	exact
WFAS	[BBLS15]	3	5	7	155	2	17	848.2	under-approximation	147	148	644.7 res log	643.9 res log	645.7 res log	under-approximation
AndOr	[CC05]	4	4	14	71	4	6	timeout	under-approximation	4	5	timeout log	timeout log	-	under-approximation
Flip-flop	[CC07]	6	6	15	165	5	11	686.6	exact	24	25	552.3 res log	473.7 res log	465.8 res log	exact
Sched5	[LSAF14]	12	21	16	328	12	20	timeout	under-approximation	80	81	timeout log	timeout log	timeout log	under-approximation
simop	[ACDFR09]	5	9	7	254	5	18	timeout	under-approximation	48	49	timeout log	timeout log	timeout log	under-approximation
train-gate		3	4	12	207	3	29	timeout	under-approximation	180	181	441.3 res log	354 res log	314.3 res log	exact
coffee	[Andre18]	1	3	7	36	1	5	346.3	under-approximation	5	6	473.3 res log	475.2 res log	-	under-approximation
CUBPTA1	[ANPS17]	1	3	9	101	1	80	0.98	exact	80	81	2.36 res log	1.63 res log	1.54 res log	exact
JLR13	[JLR15]	1	3	8	24	1	5	0.53	exact	5	6	1.11 res log	1.12 res log	-	exact

Description of the Case Studies

CSMA/CD

This is a model of the CSMA/CD proposed in [KNSW07] and modeled for the PRISM model checker. The version we consider replaces probabilities with non-determinism.

Fischer

This is a model of Fischer’s mutual exclusion protocol proposed in [AHV93].

RCP (Root Contention Protocol)

This is a model of IEEE 1394 Root Contention Protocol [CS01].

WFAS (wireless fire alarm system)

This is a model of a wireless fire alarm system studied in [BBLS15].

AndOr circuit

This small asynchronous circuit consists in an AND gate connected to an OR gate in a cyclic manner; its behavior is studied in [CC05].

Flip-flop circuit

This asynchronous circuit consists of several gates connected to each other in a cyclic manner; its behavior is studied in [CC07].

Sched5

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

SIMOP

This is a model of a networked automation system studied in [ACDFR09].

Train-gate-controller

This is a model of a train-gate-controller from here.

coffee

This is a model of a simple coffee machine used as a teaching example.

CUBPTA1

This is a toy case study to illustrate and test CUB-PTAs.

JLR15

This is a case study studied in [JLR15].

Algorithms used

For all non-distributed case studies, the following commands were used:

> ./imitator case_study.imi -mode LoopSynth -output-result -time-limit 3600

> ./imitator case_study.imi -mode NZCUBcheck -output-result -time-limit 3600

> ./imitator case_study.imi -mode NZCUBtrans -output-result -time-limit 3600

For the distributed case studies, the following commands were used:

> ./imitator case_study.imi -mode NZCUBtrans -merge -incl -output-result -time-limit 3600 -depth-limit 200

> ./patator case_study.imi -mode NZCUBtransdist -merge -incl -output-result -time-limit 3600 -depth-limit 200

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.
[AFKS12]: Étienne André, Laurent Fribourg, Ulrich Kühne and Romain Soulat. IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems. In Dimitra Giannakopoulou and Dominique Méry (eds.), FM’12, LNCS 7436, Springer, pages 33–36, August 2012. (English) [PDF | PDF (author version) | BibTeX]🌐
[AHV93]: Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601.
[ANPS17]: Étienne André, Nguyễn Hoàng Gia, Laure Petrucci and Sun Jun. Parametric model checking timed automata under non-Zenoness assumption. In Clark Barrett, Misty Davies and Temesghen Kahsai (eds.), NFM’17, Springer LNCS 10227, pages 35–51, May 2017. (English) [BibTeX | Slides]
[Andre18]: Étienne André. A benchmarks library for parametric timed model checking. In Cyrille Artho and Peter Csaba Ölveczky (eds.), FTSCS’18, Springer CCIS 1008, pages 75–83, November 2018. Acceptance rate: 45%. DOI: 10.1007/978-3-030-12988-0_5 (English) [PDF (author version) | BibTeX | data | Slides]🌐
[BBLS15]: Nikola Beneš, Peter Bezděk, Kim Guldstrand Larsen, Jirí Srba: Language Emptiness of Continuous-Time Parametric Timed Automata. In ICALP 2015, Part II, volume 9135 of LNCS, pages 69-81. Springer, 2015.
[CC04]: Robert Clarisó, Jordi Cortadella. Verification of timed circuits with symbolic delays. In ASP-DAC 2004: 628-633, 2004.
[CC05]: Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD’05, 2005.
[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).
[JLR15]: Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for real-time systems. IEEE Transactions on Software Engeneering 41(5): 445-461 (2015).
[KNSW07]: Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, and Fuzhi Wang. Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, 205(7), pages 1027-1077. July 2007.
[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é