The Quantitative Verification Benchmark Set

Arnd  Hartmanns; Michaela Klauck; David Parker; Tim Quatmann; Enno J.J. Ruijters

doi:10.1007/978-3-030-17462-0_20

The Quantitative Verification Benchmark Set

Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, Enno J.J. Ruijters

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

48 Citations (Scopus)

134 Downloads (Pure)

Abstract

We present an extensive collection of quantitative models to facilitate the development, comparison, and benchmarking of new verification algorithms and tools. All models have a formal semantics in terms of extensions of Markov chains, are provided in the Jani format, and are documented by a comprehensive set of metadata. The collection is highly diverse: it includes established probabilistic verification and planning benchmarks, industrial case studies, models of biological systems, dynamic fault trees, and Petri net examples, all originally specified in a variety of modelling languages. It archives detailed tool performance data for each model, enabling immediate comparisons between tools and among tool versions over time. The collection is easy to access via a client-side web application at qcomp.org with powerful search and visualisation features. It can be extended via a Git-based submission process, and is openly accessible according to the terms of the CC-BY license.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
Editors	Lijun Zhang, Tomáš Vojnar
Publisher	Springer
Pages	344-350
Number of pages	7
ISBN (Electronic)	978-3-030-17462-0
ISBN (Print)	978-3-030-17461-3
DOIs	https://doi.org/10.1007/978-3-030-17462-0_20
Publication status	Published - 4 Apr 2019
Event	25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 - Charles University, Prague, Czech Republic Duration: 6 Apr 2019 → 11 Apr 2019 Conference number: 25

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	11427
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019
Abbreviated title	TACAS 2019
Country/Territory	Czech Republic
City	Prague
Period	6/04/19 → 11/04/19
Other	held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019

Access to Document

10.1007/978-3-030-17462-0_20Licence: CC BY

HartmannsQuantitativeVerificationFinal published version, 1.11 MBLicence: CC BY

Cite this

Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., & Ruijters, E. J. J. (2019). The Quantitative Verification Benchmark Set. In L. Zhang, & T. Vojnar (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (pp. 344-350). (Lecture Notes in Computer Science; Vol. 11427). Springer. https://doi.org/10.1007/978-3-030-17462-0_20

Hartmanns, Arnd ; Klauck, Michaela ; Parker, David et al. / The Quantitative Verification Benchmark Set. Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. editor / Lijun Zhang ; Tomáš Vojnar. Springer, 2019. pp. 344-350 (Lecture Notes in Computer Science).

@inproceedings{05729189c54343f480d027e7752e63fe,

title = "The Quantitative Verification Benchmark Set",

abstract = "We present an extensive collection of quantitative models to facilitate the development, comparison, and benchmarking of new verification algorithms and tools. All models have a formal semantics in terms of extensions of Markov chains, are provided in the Jani format, and are documented by a comprehensive set of metadata. The collection is highly diverse: it includes established probabilistic verification and planning benchmarks, industrial case studies, models of biological systems, dynamic fault trees, and Petri net examples, all originally specified in a variety of modelling languages. It archives detailed tool performance data for each model, enabling immediate comparisons between tools and among tool versions over time. The collection is easy to access via a client-side web application at qcomp.org with powerful search and visualisation features. It can be extended via a Git-based submission process, and is openly accessible according to the terms of the CC-BY license.",

author = "Arnd Hartmanns and Michaela Klauck and David Parker and Tim Quatmann and Ruijters, {Enno J.J.}",

note = "Funding Information: Authors are listed alphabetically. This work was supported by DFG grant 389792660 (part of CRC 248), ERC Advanced Grants 695614 (POWVER) and 781914 (FRAPPANT), NWO and BetterBe grant 628.010.006, and NWO VENI grant 639.021.754. Publisher Copyright: {\textcopyright} The Author(s) 2019.; 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 , TACAS 2019 ; Conference date: 06-04-2019 Through 11-04-2019",

year = "2019",

month = apr,

day = "4",

doi = "10.1007/978-3-030-17462-0_20",

language = "English",

isbn = "978-3-030-17461-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "344--350",

editor = "Lijun Zhang and Tom{\'a}{\v s} Vojnar",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings",

address = "Germany",

}

Hartmanns, A, Klauck, M, Parker, D, Quatmann, T & Ruijters, EJJ 2019, The Quantitative Verification Benchmark Set. in L Zhang & T Vojnar (eds), Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Lecture Notes in Computer Science, vol. 11427, Springer, pp. 344-350, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 , Prague, Czech Republic, 6/04/19. https://doi.org/10.1007/978-3-030-17462-0_20

The Quantitative Verification Benchmark Set. / Hartmanns, Arnd ; Klauck, Michaela; Parker, David et al.
Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. ed. / Lijun Zhang; Tomáš Vojnar. Springer, 2019. p. 344-350 (Lecture Notes in Computer Science; Vol. 11427).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - The Quantitative Verification Benchmark Set

AU - Hartmanns, Arnd

AU - Klauck, Michaela

AU - Parker, David

AU - Quatmann, Tim

AU - Ruijters, Enno J.J.

N1 - Conference code: 25

PY - 2019/4/4

Y1 - 2019/4/4

N2 - We present an extensive collection of quantitative models to facilitate the development, comparison, and benchmarking of new verification algorithms and tools. All models have a formal semantics in terms of extensions of Markov chains, are provided in the Jani format, and are documented by a comprehensive set of metadata. The collection is highly diverse: it includes established probabilistic verification and planning benchmarks, industrial case studies, models of biological systems, dynamic fault trees, and Petri net examples, all originally specified in a variety of modelling languages. It archives detailed tool performance data for each model, enabling immediate comparisons between tools and among tool versions over time. The collection is easy to access via a client-side web application at qcomp.org with powerful search and visualisation features. It can be extended via a Git-based submission process, and is openly accessible according to the terms of the CC-BY license.

AB - We present an extensive collection of quantitative models to facilitate the development, comparison, and benchmarking of new verification algorithms and tools. All models have a formal semantics in terms of extensions of Markov chains, are provided in the Jani format, and are documented by a comprehensive set of metadata. The collection is highly diverse: it includes established probabilistic verification and planning benchmarks, industrial case studies, models of biological systems, dynamic fault trees, and Petri net examples, all originally specified in a variety of modelling languages. It archives detailed tool performance data for each model, enabling immediate comparisons between tools and among tool versions over time. The collection is easy to access via a client-side web application at qcomp.org with powerful search and visualisation features. It can be extended via a Git-based submission process, and is openly accessible according to the terms of the CC-BY license.

UR - http://www.scopus.com/inward/record.url?scp=85064956253&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-17462-0_20

DO - 10.1007/978-3-030-17462-0_20

M3 - Conference contribution

SN - 978-3-030-17461-3

T3 - Lecture Notes in Computer Science

SP - 344

EP - 350

BT - Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings

A2 - Zhang, Lijun

A2 - Vojnar, Tomáš

PB - Springer

T2 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019

Y2 - 6 April 2019 through 11 April 2019

ER -

Hartmanns A, Klauck M, Parker D, Quatmann T, Ruijters EJJ. The Quantitative Verification Benchmark Set. In Zhang L, Vojnar T, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Springer. 2019. p. 344-350. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-17462-0_20

The Quantitative Verification Benchmark Set

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this