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

Ernst Moritz Hahn; Arnd Hartmanns; Christian Hensel; Michaela Klauck; Joachim Klein; Jan Kretínský; David Parker; Tim Quatmann; Enno Ruijters; Marcel Steinmetz

doi:10.1007/978-3-030-17502-35

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

Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Kretínský, David Parker, Tim Quatmann, Enno Ruijters, Marcel Steinmetz

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

32 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	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
Subtitle of host publication	TOOLympics, Held as Part of ETAPS 2019, Proceedings
Editors	Bernhard Steffen, Fabrice Kordon, Dirk Beyer, Marieke Huisman
Pages	69-92
Number of pages	24
DOIs	https://doi.org/10.1007/978-3-030-17502-35
Publication status	Published - 2019

Access to Document

10.1007/978-3-030-17502-35

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

Cite this

Hahn, E. M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kretínský, J., Parker, D., Quatmann, T., Ruijters, E., & Steinmetz, M. (2019). The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). In B. Steffen, F. Kordon, D. Beyer, & M. Huisman (Eds.), 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: TOOLympics, Held as Part of ETAPS 2019, Proceedings (pp. 69-92) https://doi.org/10.1007/978-3-030-17502-35

Hahn, Ernst Moritz ; Hartmanns, Arnd ; Hensel, Christian et al. / The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). 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: TOOLympics, Held as Part of ETAPS 2019, Proceedings. editor / Bernhard Steffen ; Fabrice Kordon ; Dirk Beyer ; Marieke Huisman. 2019. pp. 69-92

@inproceedings{4598db3026a441e9bfd2cf231ea9041d,

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

abstract = "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.",

author = "Hahn, {Ernst Moritz} and Arnd Hartmanns and Christian Hensel and Michaela Klauck and Joachim Klein and Jan Kret{\'i}nsk{\'y} and David Parker and Tim Quatmann and Enno Ruijters and Marcel Steinmetz",

year = "2019",

doi = "10.1007/978-3-030-17502-35",

language = "English",

isbn = "9783030175016",

pages = "69--92",

editor = "Bernhard Steffen and Fabrice Kordon and Dirk Beyer and Marieke Huisman",

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",

}

Hahn, EM, Hartmanns, A, Hensel, C, Klauck, M, Klein, J, Kretínský, J, Parker, D, Quatmann, T, Ruijters, E & Steinmetz, M 2019, The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). in B Steffen, F Kordon, D Beyer & M Huisman (eds), 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: TOOLympics, Held as Part of ETAPS 2019, Proceedings. pp. 69-92. https://doi.org/10.1007/978-3-030-17502-35

The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). / Hahn, Ernst Moritz; Hartmanns, Arnd; Hensel, Christian et al.
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: TOOLympics, Held as Part of ETAPS 2019, Proceedings. ed. / Bernhard Steffen; Fabrice Kordon; Dirk Beyer; Marieke Huisman. 2019. p. 69-92.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Hahn, Ernst Moritz

AU - Hartmanns, Arnd

AU - Hensel, Christian

AU - Klauck, Michaela

AU - Klein, Joachim

AU - Kretínský, Jan

AU - Parker, David

AU - Quatmann, Tim

AU - Ruijters, Enno

AU - Steinmetz, Marcel

PY - 2019

Y1 - 2019

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.

AB - 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.

U2 - 10.1007/978-3-030-17502-35

DO - 10.1007/978-3-030-17502-35

M3 - Conference contribution

SN - 9783030175016

SP - 69

EP - 92

BT - 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

A2 - Steffen, Bernhard

A2 - Kordon, Fabrice

A2 - Beyer, Dirk

A2 - Huisman, Marieke

ER -

Hahn EM, Hartmanns A, Hensel C, Klauck M, Klein J, Kretínský J et al. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). In Steffen B, Kordon F, Beyer D, Huisman M, editors, 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: TOOLympics, Held as Part of ETAPS 2019, Proceedings. 2019. p. 69-92 doi: 10.1007/978-3-030-17502-35

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

Abstract

Access to Document

Fingerprint

Cite this