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
  • CSL
  • Expected Rewards
  • Conditional Probabilities
Read more

News

12 December 2017

New version 1.2.0

We are happy to announce the next stable release of Storm in version 1.2.0.

Read more
10 August 2017

New version 1.1.0

As Storm has quite some new features and its dependencies (noticably, carl) moved forward as well, we are happy to announce Storm version 1.1.0.

Read more
12 April 2017

Storm at CAV 2017

We are delighted that a tool-paper describing Storm has been accepted for presentation at Computer Aided Verification 2017 in Heidelberg, Germany.

Read more