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.

Storm is built around discrete- and continuous-time Markov models:

• Discrete-time Markov Chains
• Markov Decision Processes
• Continuous-time Markov Chains
• Markov Automata
• Parametric Markov Models
• Partially Observable Markov Models

Storm supports several types of input:

• PRISM
• JANI
• GSPNs
• DFTs
• cpGCL
• explicit

Supported model checking queries include

• Reachability and Reach-Avoid Probabilities
• PCTL, CSL, and LTL Specifications
• Expected Accumulated Rewards
• Long-run Average Rewards
• Conditional Probabilities
• Multi-objective Analysis