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 |
|---|---|---|
| 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 |
| Case Study | Reference | GrML Input |