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.

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

Input languages

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

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

News

02 August 2022

Storm featured in UAI Tutorial

Storm has recently been featured in a tutorial on probabilistic verification at UAI 2022.


31 July 2022

New version 1.7.0

We are happy to announce the next stable releases of Storm and stormpy in version 1.7.0.


11 June 2022

10 years of Storm

We celebrate the 10th anniversary of Storm.