IMITATOR

The IMITATOR benchmarks library

This page contains

  1. A pointer to the "official" IMITATOR benchmarks library v1 [Andre18]
  2. Links to several lists of benchmarks and experimental raw data from the IMITATOR publications
  3. A link to the full list of benchmarks on GitHub

1) The official benchmarks library

The official benchmarks library in version 2.1 [AMP21] is available there. These models have been accumulated over the years from scientific publications, and from industrial collaborations.

Former version

The former version of the library (in version 1) [Andre18] is available there.

2) Lists of benchmarks with experimental data

We give below lists of benchmarks associated with publications related to algorithms integrated in IMITATOR, or to case studies verified using IMITATOR.

Each page associated with a publication contains the list of benchmarks, the binaries and source of the IMITATOR version used to compute the result, and all raw experimental data.

Publication Purpose List of benchmarks
[ACFJL21] Parametric schedulability analysis of a launcher flight control system benchmarks
[AAPP21] Parametric cycle synthesis benchmarks [✔️ artifact evaluated]
[AK20] Parametric non-interference in timed automata benchmarks
[AS19] Parametric timed model checking for guaranteeing timed opacity benchmarks [✔️ artifact evaluated]
[ALRS19] Parametric analyses of attack-fault trees benchmarks
[ACFJL19] Parametric schedulability analysis of a launcher flight control system benchmarks
[AAGR19] Repairing timed automata clock guards through abstraction and testing models
[ABPP19] Minimal-Time Synthesis for Parametric Timed Automata benchmarks [✔️ artifact evaluated]
[WA19] Parametric Timed Pattern Matching with Automata-Based Skipping benchmarks
[AHW18] Parametric timed pattern matching benchmarks
[ALin17] Learning-based compositional synthesis benchmarks
[ANPS17] Non-Zeno parametric model checking benchmarks
[ACN15] Enhanced distributed cartography benchmarks
[SAL15] Solution to the Thales FMTV challenge benchmark
[ALNS15] New algorithms PRP and PRPC benchmarks
[AFS13atva] Inverse method and state merging benchmarks
[AFKS12] Tool paper 2.5 benchmarks
[Andre10infinity] Tool paper 2.0 benchmarks
[Andre09ictac] Tool paper 1.0 benchmarks

3) The full IMITATOR benchmark library

The entire (and raw) IMITATOR benchmark library is available on GitHub (in directory "benchmarks").

References

[AAGR19]
Étienne André, Paolo Arcaini, Angelo Gargantini and Marco Radavelli. Repairing timed automata clock guards through abstraction and testing. In Dirk Beyer and Chantal Keller (eds.), TAP’19, Springer LNCS 11823, pages 129–146, October 2019. DOI: 10.1007/978-3-030-31157-5_9 (English) [PDF (author version) | BibTeX | data]🌐
[AAPP21]
Étienne André, Jaime Arias, Laure Petrucci and Jaco van de Pol. Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In Jan Friso Groote and Kim G. Larsen (eds.), TACAS’21, March 2021. To appear. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [data]
[ABPP19]
Étienne André, Vincent Bloemen, Laure Petrucci and Jaco van de Pol. Minimal-Time Synthesis for Parametric Timed Automata. In Tomáš Vojnar and Lijun Zhang (eds.), TACAS’19, Springer LNCS 11428, pages 211–228, April 2019. Acceptance rate: 30%. DOI: 10.1007/978-3-030-17465-1_12 Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [PDF | PDF (author version) | BibTeX | data]🌐
[ACFJL19]
Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray and David Lesens. Parametric schedulability analysis of a launcher flight control system under reactivity constraints. In Jörg Keller and Wojciech Penczek (eds.), ACSD’19, IEEE, pages 13–22, June 2019. DOI: 10.1109/ACSD.2019.00006 (English) [PDF (author version) | BibTeX | data]🌐
[ACFJL21]
Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray and David Lesens. Parametric schedulability analysis of a launcher flight control system under reactivity constraints. Fundamenta Informatica. 2021. To appear.
[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]
[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]🌐
[AFS13atva]
Étienne André, Laurent Fribourg and Romain Soulat. Merge and Conquer: State Merging in Parametric Timed Automata. In Hung Dang-Van and Mizuhito Ogawa (eds.), ATVA’13, LNCS 8172, Springer, pages 381–396, October 2013. [PDF (author version) | PDF (long author version) | BibTeX | Slides]
[AHW18]
Étienne André, Ichiro Hasuo and Masaki Waga (和賀 正樹). Offline timed pattern matching under uncertainty. In Anthony Widjaja Lin and Jun Sun (eds.), ICECCS’18, IEEE CPS, pages 10–10, December 2018. (English) [BibTeX | Slides]
[AK20]
Étienne André and Aleksander Kryukov. Parametric non-interference in timed automata. In Yi Li and Alan Liew (eds.), ICECCS’20, October 2020. To appear. (English) [PDF (author version) | data]🌐
[ALNS15]
Étienne André, Giuseppe Lipari, Nguyễn Hoàng Gia and Sun Youcheng. Reachability Preservation Based Parameter Synthesis for Timed Automata. In Klaus Havelund, Gerard Holzmann, Rajeev Joshi (eds.), NFM’15, LNCS 9058, Springer, pages 50–65, April 2015. (English) [PDF | PDF (author version) | BibTeX | Slides]
[ALRS19]
Étienne André, Didier Lime, Mathias Ramparison and Mariëlle Stoelinga. Parametric analyses of attack-fault trees. In Jörg Keller and Wojciech Penczek (eds.), ACSD’19, IEEE, pages 33–42, June 2019. DOI: 10.1109/ACSD.2019.00008 (English) [PDF (author version) | BibTeX | data]🌐
[ALin17]
Étienne André and Lin Shang-Wei (林尚威). Learning-based compositional parameter synthesis for event-recording automata. In Ahmed Bouajjani and Alexandra Silva (eds.), FORTE’17, Springer LNCS 10321, pages 17–32, June 2017. (English) [PDF (author version) | BibTeX | Slides]🌐
[AMP21]
Étienne André, Dylan Marinho and Jaco van de Pol. A Benchmarks Library for Extended Timed Automata. In Frédéric Loulergue and Franz Wotawa (eds.), TAP’21, Springer LNCS 12740, pages 39-50, June 2021. DOI: 10.1007/978-3-030-79379-1_3 (English) [PDF (author version) | BibTeX | data | Slides]🌐
[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]
[AS19]
Étienne André and Sun Jun. Parametric timed model checking for guaranteeing timed opacity. In Yu-Fang Chen, Chih-Hong Cheng and Javier Esparza (eds.), ATVA’19, Springer LNCS 11781, pages 115–130, October 2019. DOI: 10.1007/978-3-030-31784-3_7 (English) [PDF (author version) | BibTeX | data | Slides]🌐
[Andre09ictac]
Étienne André. IMITATOR: A Tool for Synthesizing Constraints on Timing Bounds of Timed Automata. In Martin Leucker and Carroll Morgan (eds.), ICTAC’09, LNCS 5684, Springer, pages 336–342, August 2009. [PDF (published version) | PDF (author version) | BibTeX | Slides]
[Andre10infinity]
Étienne André. IMITATOR II: A Tool for Solving the Good Parameters Problem in Timed Automata. In Yu-Fang Chen and Ahmed Rezine (eds.), INFINITY’10, Electronic Proceedings in Theoretical Computer Science 39, pages 91–99, 2010. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [PDF (published version) | 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]🌐
[SAL15]
Sun Youcheng, Étienne André and Giuseppe Lipari. Verification of Two Real-Time Systems Using Parametric Timed Automata. In Sophie Quinton and Tullio Vardanega (eds.), WATERS’15, July 2015. (English) [PDF (author version)]
[WA19]
Masaki Waga (和賀 正樹) and Étienne André. Online Parametric Timed Pattern Matching with Automata-Based Skipping. In Julia Badger and Kristin Yvonne Rozier (eds.), NFM’19, Springer LNCS 11460, pages 371–389, May 2019. DOI: 10.1007/978-3-030-20652-9_26 (English) [PDF | PDF (author version) | BibTeX | data]🌐