IMITATOR

The IMITATOR benchmarks library

The IMITATOR benchmarks library

This page presents the official IMITATOR benchmarks library. These models have been accumulated over the years from scientific publications, and from industrial collaborations.

As of today, the library contains 34 benchmarks with 80 different models and 122 properties.

The library is under constant construction. It will be soon enriched with version numbers to make clear which version of the library one refers to.

New metrics will soon appear too (number of parametric clocks, size of the state space using the symbolic zone graph…)

For robustness analysis, the reference valuation can be obtained in the IM column.

Benchmark Source Categories Metrics Property Execution
Academic Automotive Educ. Hardw. Industrial ProdCons Protocol RTS Sched Toy |PTA| |X| |P| |D| |L| |Act| L/U? Inv? SW? Reach. Safety AF Pattern Opt. Cycle IM time
And-Or [CC05] yesnonoyesnononononono 4 4 12 0 27 8 yes no nononoyesnoyesno 3.01 s
Bounded retransmission protocol [DKRT97] yesnononoyesnoyesyesnono 6 7 2 12 22 12 Not L/U yes no noyesnonononono 248.35 s
Not-Not-And circuit [ACR16] yesnonoyesnononononono 5 5 6 0 8 20 L/U-PTA yes no noyesnonononono ?
Not-Not-And circuit [ACR16] yesnonoyesnononononono 5 5 6 0 8 20 L/U-PTA yes no nonononononoyes ?
3NotAnd [ACR16] yesnonoyesnononononono 5 5 10 0 22 9 L/U-PTA yes no noyesnonononono ?
3NotAnd [ACR16] yesnonoyesnononononono 5 5 10 0 22 9 L/U-PTA yes no nonononononoyes ?
3NotAnd [ACR16] yesnonoyesnononononono 5 5 10 0 22 9 L/U-PTA yes no nonononononoyes H.S.
coffee machine nonoyesnonononononoyes 1 2 3 0 4 4 Not L/U yes no yesnononononono ?
coffee machine nonoyesnonononononoyes 1 2 3 0 4 4 Not L/U yes no nonoyesnononono ?
coffee machine nonoyesnonononononoyes 1 2 3 0 4 4 Not L/U yes no nonononononoyes ?
Coffee machine + drinker nonoyesnonononononoyes 2 4 6 1 8 4 Not L/U yes no noyesnonononono ?
Coffee machine + drinker nonoyesnonononononoyes 2 4 6 1 8 4 Not L/U yes no nonononononoyes ?
Coffee machine + unbounded drinker nonoyesnonononononoyes 2 4 6 1 8 4 Not L/U yes no noyesnonononono ?
Coffee machine + unbounded drinker nonoyesnonononononoyes 2 4 6 1 8 4 Not L/U yes no nonononononoyes ?
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 19 9 Not L/U yes no yesnononononono H.S.
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 19 9 Not L/U yes no nonoyesnononono ?
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 19 9 Not L/U yes no nonononononoyes ?
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 525 9 Not L/U yes no yesnononononono H.S.
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 525 9 Not L/U yes no nonoyesnononono ?
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 525 9 Not L/U yes no nonononononoyes ?
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 4115 9 Not L/U yes no yesnononononono H.S.
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 4115 9 Not L/U yes no nonoyesnononono ?
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 4115 9 Not L/U yes no nonononononoyes ?
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 8213 9 Not L/U yes no yesnononononono H.S.
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 8213 9 Not L/U yes no nonoyesnononono ?
CSMA/CD [KNSW07] yesnononoyesnoyesyesnono 3 3 3 0 8213 9 Not L/U yes no nonononononoyes ?
Fischer (L/U-PTA) [AHV93] yesnononononoyesyesnono 3 2 4 0 10 10 L/U-PTA no no noyesnonononono 0.04 s
Fischer (L/U-PTA) [HRSV02] yesnononononoyesyesnono 2 2 4 1 8 0 L/U-PTA yes no noyesnonononono H.S.
Fischer (L/U-PTA) [HRSV02] yesnononononoyesyesnono 2 2 4 1 8 0 L/U-PTA yes no nonononononoyes ?
Fischer (L/U-PTA) [HRSV02] yesnononononoyesyesnono 3 3 4 1 12 0 L/U-PTA yes no noyesnonononono H.S.
Fischer (L/U-PTA) [HRSV02] yesnononononoyesyesnono 3 3 4 1 12 0 L/U-PTA yes no nonononononoyes ?
Fischer (timed CSP) yesnononononoyesyesnono 2 2 2 2 10 12 L/U-PTA yes no noyesnonononono ?
Fischer (timed CSP) yesnononononoyesyesnono 2 2 2 2 10 12 L/U-PTA yes no nonononononoyes H.S.
Fischer (timed CSP) yesnononononoyesyesnono 3 3 2 2 15 18 L/U-PTA yes no noyesnonononono ?
Fischer (timed CSP) yesnononononoyesyesnono 3 3 2 2 15 18 L/U-PTA yes no nonononononoyes H.S.
Fischer (unknown origin) yesnononononoyesyesnono 3 2 2 1 9 11 L/U-PTA yes no noyesnonononono ?
Fischer (unknown origin) yesnononononoyesyesnono 3 2 2 1 9 11 L/U-PTA yes no nonononononoyes ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 4 2 2 1 13 8 L/U-PTA no no noyesnonononono ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 4 2 2 1 13 8 L/U-PTA no no nonononononoyes ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 5 3 2 1 18 12 L/U-PTA no no noyesnonononono ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 5 3 2 1 18 12 L/U-PTA no no nonononononoyes ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 6 4 2 1 23 16 L/U-PTA no no noyesnonononono ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 6 4 2 1 23 16 L/U-PTA no no nonononononoyes ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 7 5 2 1 28 20 L/U-PTA no no noyesnonononono ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 7 5 2 1 28 20 L/U-PTA no no nonononononoyes ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 12 10 2 1 53 40 L/U-PTA no no noyesnonononono ?
Fischer-PS08 [PS08] yesnononononoyesyesnono 12 10 2 1 53 40 L/U-PTA no no nonononononoyes ?
Flip-flop [CC07] yesnonoyesnononononono 5 5 2 0 52 12 U-PTA yes no noyesnonononono 0.031 s
Flip-flop [CC07] yesnonoyesnononononono 5 5 2 0 52 12 U-PTA yes no nonononononoyes ?
Flip-flop [CC07] yesnonoyesnononononono 5 5 4 0 52 12 U-PTA yes no noyesnonononono ?
Flip-flop [CC07] yesnonoyesnononononono 5 5 4 0 52 12 U-PTA yes no nonononononoyes ?
Flip-flop [CC07] yesnonoyesnononononono 5 5 12 0 52 12 U-PTA yes no noyesnonononono 23.07 s
Flip-flop [CC07] yesnonoyesnononononono 5 5 12 0 52 12 U-PTA yes no nonononononoyes ?
Jobshop 2-4 nonononononononoyesno 2 2 8 4 18 4 Not L/U yes no yesnononoyesnono ?
Jobshop 2-4 nonononononononoyesno 2 2 8 4 18 4 Not L/U yes no nonononononoyes ?
Jobshop 2-4 nonononononononoyesno 2 3 12 4 27 3 Not L/U yes no yesnononoyesnono 5.58 s
Jobshop 2-4 nonononononononoyesno 2 3 12 4 27 3 Not L/U yes no nonononononoyes ?
Jobshop 2-4 nonononononononoyesno 4 4 16 4 36 4 Not L/U yes no yesnononoyesnono ?
Jobshop 2-4 nonononononononoyesno 4 4 16 4 36 4 Not L/U yes no nonononononoyes T.O.
Cooking noodles nonoyesnonononononoyes 1 2 2 0 4 4 Not L/U yes no noyesnonononono ?
Nuclear plant nonoyesnonononononoyes 1 2 4 0 6 6 Not L/U yes no noyesnonononono ?
Packaging yesnonononoyesnononono 3 2 2 0 10 6 L/U-PTA yes no yesnononononono ?
Packaging yesnonononoyesnononono 3 2 2 0 10 6 L/U-PTA yes no nonononononoyes ?
Producer-consumer [KP12] yesnonononoyesnononono 5 5 6 0 16 11 L/U-PTA yes no yesnononononono T.O.
Producer-consumer [KP12] yesnonononoyesnononono 5 5 6 0 20 15 L/U-PTA yes no yesnononononono ?
Producer-consumer [KP12] yesnonononoyesnononono 6 6 6 0 18 12 L/U-PTA yes no yesnononononono ?
Producer-consumer [KP12] yesnonononoyesnononono 6 6 6 0 21 15 L/U-PTA yes no yesnononononono ?
Root contention protocol [CS01] nonononoyesnoyesyesnono 5 6 5 6 48 16 L/U-PTA yes no yesnononononono 1.07 s
Root contention protocol [CS01] nonononoyesnoyesyesnono 5 6 5 6 48 16 L/U-PTA yes no nonoyesnononono ?
Root contention protocol [CS01] nonononoyesnoyesyesnono 5 6 5 6 48 16 L/U-PTA yes no nonoyesnononono ?
SSLAF14 test 1 [SSLAF13] nonononononoyesyesnono 7 16 2 2 42 23 Not L/U yes yes noyesnonononono 0.33 s
SSLAF14 test 2 [SSLAF13] nonononononoyesyesnono 6 14 2 4 45 26 Not L/U yes yes noyesnonononono T.O.
NP-FPS-3tasks [JLR13] yesnononononoyesyesnono 4 6 2 0 17 3 Not L/U yes no noyesnonononono ?
NP-FPS-3tasks [JLR13] yesnononononoyesyesnono 4 6 2 0 17 3 U-PTA yes no noyesnonononono 1.03 s
NP-FPS-3tasks [JLR13] yesnononononoyesyesnono 4 6 2 0 17 3 U-PTA yes no noyesnonononono ?
NP-FPS-3tasks [JLR13] yesnononononoyesyesnono 4 6 2 0 17 3 U-PTA yes no noyesnonononono ?
NP-FPS-3tasks [JLR13] yesnononononoyesyesnono 4 6 2 0 17 3 U-PTA yes no noyesnonononono 65.23 s
SLAF14 [SLAF14] yesnononononoyesyesnono 8 13 2 3 47 17 Not L/U yes yes noyesnonononono 1.49 s
SLAF14 [SLAF14] yesnononononoyesyesnono 12 21 2 0 153 29 Not L/U yes yes noyesnonononono 14.61 s
FMTV Challenge 1A [SAL15] nonononoyesnoyesyesnono 3 3 3 5 15 9 Not L/U yes no yesnononoyesnono 6.97 s
FMTV Challenge 1A [SAL15] nonononoyesnoyesyesnono 3 3 3 7 15 12 Not L/U yes no yesnononoyesnono 87.39 s
FMTV Challenge 2 [SAL15] nonononoyesnoyesyesnono 6 9 2 0 87 21 Not L/U yes yes yesnononoyesnono 1.61 s
SIMOP [ACDFR09] nonononoyesnonononono 5 8 2 0 46 16 Not L/U yes no yesnononononono ?
SIMOP [ACDFR09] nonononoyesnonononono 5 8 2 0 46 16 Not L/U yes no nonononononoyes ?
SIMOP [ACDFR09] nonononoyesnonononono 5 8 3 0 46 16 Not L/U yes no yesnononononono T.O.
SIMOP [ACDFR09] nonononoyesnonononono 5 8 3 0 46 16 Not L/U yes no nonononononoyes ?
train1PTA nonoyesnonononononoyes 1 2 3 0 5 4 Not L/U yes no noyesnonononono ?
train1PTA nonoyesnonononononoyes 1 2 3 0 5 4 Not L/U yes no nonononononoyes ?
TrainAHV93 [AHV93] yesnonononononononono 3 3 6 0 12 8 L/U-PTA no no noyesnonononono 0.01 s
TrainAHV93 [AHV93] yesnonononononononono 3 3 6 0 12 8 L/U-PTA no no noyesnonononono ?
SPSMALL [CEFX09][Andre10] nononoyesyesnonononono 11 11 2 0 52 25 Not L/U yes no yesnononononono ?
SPSMALL [CEFX09][Andre10] nononoyesyesnonononono 11 11 2 0 52 25 Not L/U yes no nonononononoyes 0.96 s
SPSMALL [CEFX09][Andre10] nononoyesyesnonononono 11 11 26 0 52 25 Not L/U yes no yesnononononono T.O.
SPSMALL [CEFX09][Andre10] nononoyesyesnonononono 11 11 26 0 52 25 Not L/U yes no nonononononoyes ?
WFAS [BBLS15] yesnonononononononono 3 4 2 0 10 4 Not L/U yes no noyesnonononono H.S.
WFAS [BBLS15] yesnonononononononono 3 4 2 0 10 4 Not L/U yes no nonononononoyes ?
WFAS [BBLS15] yesnonononononononono 3 4 2 0 10 4 Not L/U yes no nonononononoyes ?
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 2574 10 Not L/U yes no yesnononononono 1.25 s
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 4909 10 Not L/U yes no yesnononononono ?
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 7814 10 Not L/U yes no yesnononononono ?
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 10060 10 Not L/U yes no yesnononononono ?
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 12546 10 Not L/U yes no yesnononononono ?
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 15390 10 Not L/U yes no yesnononononono ?
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 17703 10 Not L/U yes no yesnononononono ?
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 20314 10 Not L/U yes no yesnononononono ?
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 22706 10 Not L/U yes no yesnononononono ?
accel [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 25152 10 Not L/U yes no yesnononononono 12.67 s
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 1475 6 Not L/U yes no yesnononononono 0.77 s
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 2845 6 Not L/U yes no yesnononononono ?
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 4603 6 Not L/U yes no yesnononononono ?
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 5847 6 Not L/U yes no yesnononononono ?
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 7309 6 Not L/U yes no yesnononononono ?
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 9003 6 Not L/U yes no yesnononononono ?
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 10323 6 Not L/U yes no yesnononononono ?
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 11839 6 Not L/U yes no yesnononononono ?
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 13191 6 Not L/U yes no yesnononononono ?
gear [HAF14][AHW18] noyesnonoyesnonononono 2 2 3 0 14665 6 Not L/U yes no yesnononononono 7.42 s
blowup [AHW18] nononononononononoyes 2 3 5 0 208 4 Not L/U yes no yesnononononono ?
blowup [AHW18] nononononononononoyes 2 3 5 0 408 4 Not L/U yes no yesnononononono ?
blowup [AHW18] nononononononononoyes 2 3 5 0 608 4 Not L/U yes no yesnononononono ?
blowup [AHW18] nononononononononoyes 2 3 5 0 808 4 Not L/U yes no yesnononononono ?
blowup [AHW18] nononononononononoyes 2 3 5 0 1008 4 Not L/U yes no yesnononononono ?

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.
[ACR16]
Étienne André, Thomas Chatain and César Rodríguez. Preserving Partial Order Runs in Parametric Time Petri Nets. Transactions on Embedded Computing Systems 16(2), pages 43:1–43:26, December 2016. (English) [PDF | BibTeX]
[AHV93]
Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601.
[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]
[Andre10]
Étienne André. An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems. Ph.D. thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2010.
[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.
[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.
[CEFX09]
Rémy Chevallier, Emmanuelle Encrenaz-Tiphène, Laurent Fribourg, and Weiwen Xu. Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design, 34(1):59–81, 2009.
[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).
[DKRT97]
Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans: The Bounded Retransmission Protocol Must Be on Time! TACAS 1997: 416-431.
[HAF14]
Bardh Hoxha, Houssam Abbas, Georgios E. Fainekos: Benchmarks for Temporal Logic Requirements for Automotive Systems. ARCH@CPSWeek 2014: 25-30
[HRSV02]
Thomas Hune, Judi Romijn, Mariëlle Stoelinga, Frits W. Vaandrager: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52-53: 183-220 (2002)
[JLR13]
Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for timed automata. In TACAS, volume 7795 of Lecture Notes in Computer Science, pages 401–415. Springer, 2013.
[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.
[KP12]
Michał Knapik, Wojciech Penczek: Bounded Model Checking for Parametric Timed Automata. Trans. Petri Nets and Other Models of Concurrency 5: 141-159 (2012)
[PS08]
Wojciech Penczek, Maciej Szreter. SAT-based Unbounded Model Checking of Timed Automata. Fundam. Inform. 85(1-4): 425-440 (2008)
[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)]
[SLAF14]
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 145, pages 49–64, April 2014. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [PDF | BibTeX]
[SSLAF13]
Sun Youcheng, Romain Soulat, Giuseppe Lipari, Étienne André and Laurent Fribourg. Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems. In Cyrille Artho and Peter Ölveczky (eds.), FTSCS’13, Volume 419 of Communications in Computer and Information Science, Springer, pages 212–228, October 2013. (English) [PDF (author version) | Slides]