IMITATOR

IMITATOR: Experiments Data for NFM 2017

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

This page is dedicated to the case studies related to the manuscript Parametric model checking timed automata under non-Zenoness assumption by Étienne André, Hoang Gia Nguyen, Laure Petrucci and Jun Sun, published in the proceedings of the NFM’17 [ANPS17].

IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR 2.8.1-working (branch learning, build 2108, GitHub hash 3ca9b1ca7cab3271e82d852a72c922665e9b02c7).

Download

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

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 3600 true invalid 0.013 0.013 false - - 0.3 3600 74 true exact
Fischer [AHV93] 3 2 4 13 3600 true invalid 0.003 0.003 false - - 0.012 3600 20 true exact
RCP 5 6 5 48 3600 some invalid 0.013 0.013 false - - 0.348 3600 71 false under-approximation
WFAS [BBLS15] 3 4 2 10 3600 some invalid 0.009 0.009 false - - 0.246 1848 40 some exact
AndOr [CC05] 4 4 4 27 3600 some invalid 0.012 0.012 false - - 0.059 3600 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 12 21 2 153 190 false exact 0.051 0.051 false - - 1.18 3600 180 false under-approximation
simop [ACDFR09] 5 8 2 46 3600 false invalid 0.012 0.012 false - - 0.219 3600 81 false under-approximation
train-gate 4 5 9 11 3600 false invalid 0 3600 some false under-approximation 0.059 3600 23 false under-approximation
coffee 3 2 3 4 3600 some invalid 0 3600 some some under-approximation 0.012 3600 10 some under-approximation
CUBPTA1 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 3600 false invalid 0 3600 true false under-approximation 0 3600 3 false under-approximation

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.

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

Sched5

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

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 case studies, 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

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

Contact

Étienne André