Parametric Timed Automata

We give below a list of (parametric) timed automata benchmarks. They mostly come from the IMITATOR case studies, which are a list os case studies coming from both the literature and the industry. The original reference for each case study is given below.

Models

For each model, we provide its origin (as a reference) and the corresponding GrML description.

Case Study Reference GrML Input
Case Study Reference GrML Input
And Or Circuit Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD'05, 2005. AndOr.imi.grml
Bang & Olufsen procotol BangOlufsen.imi.grml
Bounded Retransmission Protocol P.R. D'Argenio, J.P. Katoen, T.C. Ruys, and G.J. Tretmans. The bounded retransmission protocol must be on time! In TACAS'97. Springer, 1997. brp.imi.grml
CSMA/CD protocol M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects of Computing, 14(3):295-318, 2003. csmacdPrism.imi.grml
Sample PTA exSITH.imi.grml
Flip-Flop circuit Robert Clarisó, Jordi Cortadella. The Octahedron Abstract Domain. In Science of Computer Programming 64(1), pages 115-139, 2007. flipflop.imi.grml
Latch circuit É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. 268 pages. latchValmem.imi.grml
SPSMALL memory Remy Chevallier, Emmanuelle Encrenaz, Laurent Fribourg, Weiwen Xu. Timed Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata. Formal Methods in System Design 34(1), pages 59-81, 2009. LSV.imi.grml
Jobshop 2 Yasmina Abdeddaïm and Oded Maler. Preemptive job-shop scheduling using stopwatch automata. In TACAS'02, pages 113-126, 2002. maler_2_4.imi.grml
Jobshop 3 Yasmina Abdeddaïm and Oded Maler. Preemptive job-shop scheduling using stopwatch automata. In TACAS'02, pages 113-126, 2002. maler_3_4.imi.grml
Jobshop 4 Yasmina Abdeddaïm and Oded Maler. Preemptive job-shop scheduling using stopwatch automata. In TACAS'02, pages 113-126, 2002. maler_4_4.imi.grml
Root Contention Protocol RCP.imi.grml
SIMOP É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. 268 pages. simop.imi.grml
SPSMALL Memory (simplified version) Remy Chevallier, Emmanuelle Encrenaz, Laurent Fribourg, Weiwen Xu. Timed Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata. Formal Methods in System Design 34(1), pages 59-81, 2009. spsmall.imi.grml
SR Latch É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. 268 pages. SRlatch.imi.grml
Train R. Alur, T. A. Henzinger, and M. Y. Vardi. Parametric real-time reasoning. In STOC'93, pages 592-601. ACM, 1993. TrainAHV93.imi.grml
WLan Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD'05, 2005. wlan.imi.grml