Skip to Main content Skip to Navigation
Conference papers

A Benchmarks Library for Extended Parametric Timed Automata

Étienne André 1, 2 Dylan Marinho 1, 2 Jaco van de Pol 3
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. In order to test the efficiency of new algorithms, a fair set of benchmarks is required. We present an extension of the IMITATOR benchmarks library, that accumulated over the years a number of case studies from academic and industrial contexts. We extend here the library with several dozens of new benchmarks; these benchmarks highlight several new features: liveness properties, extensions of (parametric) timed automata (including stopwatches or multi-rate clocks), and unsolvable toy benchmarks. These latter additions help to emphasize the limits of state-of-the-art parameter synthesis techniques, with the hope to develop new dedicated algorithms in the future.
Complete list of metadata
Contributor : Étienne André Connect in order to contact the contributor
Submitted on : Monday, June 21, 2021 - 9:02:55 AM
Last modification on : Saturday, February 5, 2022 - 3:08:38 AM



Links full text




Étienne André, Dylan Marinho, Jaco van de Pol. A Benchmarks Library for Extended Parametric Timed Automata. TAP 2021 - 15th International Conference on Tests and Proofs, Jun 2021, Virtual, Norway. pp.39-50, ⟨10.1007/978-3-030-79379-1_3⟩. ⟨hal-03265573⟩



Record views