Storm model checker
| Developer(s) | Chair for Software Modeling and Verification at RWTH Aachen University |
|---|---|
| Initial release | 2017 |
| Stable release | 1.6.3
/ November 2021 |
| Repository | github |
| Written in | C++ |
| Engine | |
| Operating system | macOS, Debian, Ubuntu |
| License | GNU General Public License Version 3 |
| Website | www |
Search Storm model checker on Amazon.
The Storm Model Checker[1] is a model checking tool used to analyze systems that exhibit random or probabilistic behavior. This is done to reveal potential system errors and thus ensure desired behavior, e.g. that a system-wide failure due to failing hardware components only occurs with a low probability. Such models can be derived, among others, from systems of distributed algorithms, security protocols, systems biology or embedded systems.
Features
The model checker has a modular structure with multiple engines to choose from that can approach verification problems with different data structures and strategies according to time and memory consumption needs[2]. Similarly, it is possible to deploy different solvers for certain problems such as SMT-Solving, equation systems and stochastic games. For interfacing, there is Stormpy, a python API.
Depending on the model type to be analyzed, there are different executables to check probability and reward properties:[2]
- storm handles a variety of Markov models such as discrete-time Markov chains, continuous-time Markov chains, both partially and fully observable Markov decision processes as well as Markov automata.
- storm-pars is used for parametric versions of discrete-time Markov chains and Markov decision processes. In addition to probability and reward properties, it can analyze the model to determine its monotonicity[3] and apply parameter space partitioning.
- storm-dft is able to analyze dynamic fault trees.
- storm-gspn operates on generalized stochastic Petri nets.
- storm-pgcl checks properties of programs written in a probabilistic extension of the Guarded Command Language
Achievements
- In 2019, Christian Hensel received the European Association of Programming Language and Systems PhD Dissertation Award 2018 for his dissertation[4] on the model checker.[5]
- Storm successfully participated in the Comparison of Tools for the Analysis of Quantitative Formal Models (QComp) as part of the international TACAS conference in both 2019[6] and 2020.[7] The competition aims to compare the verification tools' performance, versatility, and usability.
- In 2020, the model checker received the second place at the RWTH Innovation Award which honors promising inventions by the university's researchers.[8]
See also
References
- ↑ Hensel, Christian; Junges, Sebastian; Katoen, Joost-Pieter; Quatmann, Tim; Volk, Matthias (6 July 2021). "The probabilistic model checker Storm". International Journal on Software Tools for Technology Transfer. 24 (4): 589–610. doi:10.1007/s10009-021-00633-z. ISSN 1433-2787. Retrieved 4 August 2022. Unknown parameter
|s2cid=ignored (help) - ↑ 2.0 2.1 "Storm -- A Modern Probabilistic Model Checker". stormchecker.org. Retrieved 26 November 2021.
- ↑ Spel, Jip; Junges, Sebastian; Katoen, Joost-Pieter (2021). "Finding Provably Optimal Markov Chains". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer International Publishing. 12651: 173–190. doi:10.1007/978-3-030-72016-2_10. ISBN 978-3-030-72015-5. Unknown parameter
|s2cid=ignored (help) - ↑ Hensel, Christian (3 December 2018). The Probabilistic Model Checker Storm. Retrieved 26 November 2021. Search this book on
- ↑ Wortmann, Andreas. "Christian Hensel (RWTH Aachen University) wins EAPLS PhD Dissertation Award 2018". eapls.org. European Association For Programming Languages and Systems. Retrieved 25 November 2021.
- ↑ Hahn, Ernst Moritz; Hartmanns, Arnd; Hensel, Christian; Klauck, Michaela; Klein, Joachim; Křetínský, Jan; Parker, David; Quatmann, Tim; Ruijters, Enno; Steinmetz, Marcel (2019). "The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer International Publishing. 11429: 69–92. doi:10.1007/978-3-030-17502-3_5. ISBN 978-3-030-17501-6. Unknown parameter
|s2cid=ignored (help) - ↑ Budde, Carlos E.; Hartmanns, Arnd; Klauck, Michaela; Křetínský, Jan; Parker, David; Quatmann, Tim; Turrini, Andrea; Zhang, Zhen (2021). "On Correctness, Precision, and Performance in Quantitative Verification". Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. Lecture Notes in Computer Science. Springer International Publishing. 12479: 216–241. doi:10.1007/978-3-030-83723-5_15. ISBN 978-3-030-83722-8.
- ↑ "2020 Innovation Award". www.rwth-aachen.de. RWTH Aachen. Retrieved 25 November 2021.
External Links
- The official Storm model checker website
- The website for the Pyton API Stormpy
- The website of QComp, the Quantitative Verification Competition
This article "Storm model checker" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Storm model checker. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.
