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

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

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

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 |

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.

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

This is a model of IEEE 1394 Root Contention Protocol.

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

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

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

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

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

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

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

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

This is a case study studied in [JLR15].

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

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