Storm

Description

Storm is a tool for the analysis of systems involving random or probabilistic phenomena. Given an input model and a quantitative specification, it can determine whether the input model conforms to the specification. It has been designed with performance and modularity in mind.
Getting started

Modeling formalisms

Storm is built around discrete- and continuous-time Markov models:
  • Discrete Time Markov Chains
  • Markov Decision Processes
  • Continuous Time Markov Chains
  • Markov Automata
Read more

Input languages

Storm supports several types of input:
  • PRISM
  • JANI
  • GSPNs
  • DFTs
  • cpGCL
  • explicit
Read more

Properties

Storm focuses on reachability queries and its support includes
  • PCTL and CSL
  • Expected Rewards
  • Long-run Average Rewards
  • Conditional Probabilities
  • Multi-objective Model Checking
Read more

News

28 October 2021

QComp 2020 Results

Storm successfully participated in the second edition of the Comparison of Tools for the Analysis of Quantitative Formal Models (QComp 2020). The competition report is available here.

Read more
15 May 2021

Storm in Aachener Nachrichten

The newspaper Aachener Nachrichten published the article Storm findet sicherheitskritische Softwarefehler.

Read more
05 March 2021

2nd place at RWTH Innovation Award 2020

The Storm model checker has received the second place at the RWTH Innovation Award 2020. The annual awards honours ideas and technologies developed by researchers and inventors at RWTH Aachen University.

Read more