The 2019 Comparison of Tools for the Analysis of Quantitative
Formal Models - (QComp 2019 Competition Report)

D 2019

The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report)

HAHN, Ernst Moritz; Arnd HARTMANNS; Christian HENSEL; Michaela KLAUCK; Joachim KLEIN et al.

Základní údaje

Originální název

The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report)

Autoři

HAHN, Ernst Moritz; Arnd HARTMANNS; Christian HENSEL; Michaela KLAUCK; Joachim KLEIN; Jan KŘETÍNSKÝ; David PARKER; Tim QUATMANN; Enno RUIJTERS a Marcel STEINMETZ

Vydání

Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, od s. 69-92, 24 s. 2019

Nakladatel

Springer

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Organizační jednotka

Fakulta informatiky

ISBN

9783030175016

ISSN

DOI

https://doi.org/10.1007/978-3-030-17502-3_5

Změněno: 17. 3. 2025 14:43, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Quantitative formal models capture probabilistic behaviour, real-time aspects, or general continuous dynamics. A number of tools support their automatic analysis with respect to dependability or performance properties. QComp 2019 is the first, friendly competition among such tools. It focuses on stochastic formalisms from Markov chains to probabilistic timed automata specified in the Jani model exchange format, and on probabilistic reachability, expected-reward, and steady-state properties. QComp draws its benchmarks from the new Quantitative Verification Benchmark Set. Participating tools, which include probabilistic model checkers and planners as well as simulation-based tools, are evaluated in terms of performance, versatility, and usability. In this paper, we report on the challenges in setting up a quantitative verification competition, present the results of QComp 2019, summarise the lessons learned, and provide an outlook on the features of the next edition of QComp.

Citovat

HAHN, Ernst Moritz; Arnd HARTMANNS; Christian HENSEL; Michaela KLAUCK; Joachim KLEIN; Jan KŘETÍNSKÝ; David PARKER; Tim QUATMANN; Enno RUIJTERS a Marcel STEINMETZ. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III. Springer, 2019, s. 69-92. ISBN 9783030175016. Dostupné z: https://doi.org/10.1007/978-3-030-17502-3_5.

@inproceedings{2484805,
   author = {Hahn, Ernst Moritz and Hartmanns, Arnd and Hensel, Christian and Klauck, Michaela and Klein, Joachim and Křetínský, Jan and Parker, David and Quatmann, Tim and Ruijters, Enno and Steinmetz, Marcel},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III},
   doi = {https://doi.org/10.1007/978-3-030-17502-3_5},
   isbn = {9783030175016},
   pages = {69-92},
   publisher = {Springer},
   title = {The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report)},
   year = {2019}
}

TY  - CONF
ID  - 2484805
AU  - Hahn, Ernst Moritz - Hartmanns, Arnd - Hensel, Christian - Klauck, Michaela - Klein, Joachim - Křetínský, Jan - Parker, David - Quatmann, Tim - Ruijters, Enno - Steinmetz, Marcel
PY  - 2019
TI  - The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report)
PB  - Springer
SN  - 9783030175016
N2  - Quantitative formal models capture probabilistic behaviour, real-time aspects, or general continuous dynamics. A number of tools support their automatic analysis with respect to dependability or performance properties. QComp 2019 is the first, friendly competition among such tools. It focuses on stochastic formalisms from Markov chains to probabilistic timed automata specified in the Jani model exchange format, and on probabilistic reachability, expected-reward, and steady-state properties. QComp draws its benchmarks from the new Quantitative Verification Benchmark Set. Participating tools, which include probabilistic model checkers and planners as well as simulation-based tools, are evaluated in terms of performance, versatility, and usability. In this paper, we report on the challenges in setting up a quantitative verification competition, present the results of QComp 2019, summarise the lessons learned, and provide an outlook on the features of the next edition of QComp.
ER  -

HAHN, Ernst Moritz; Arnd HARTMANNS; Christian HENSEL; Michaela KLAUCK; Joachim KLEIN; Jan KŘETÍNSKÝ; David PARKER; Tim QUATMANN; Enno RUIJTERS a Marcel STEINMETZ. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). In \textit{Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III}. Springer, 2019, s.~69-92. ISBN~9783030175016. Dostupné z: https://doi.org/10.1007/978-3-030-17502-3\_{}5.

Přehled o publikaci