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

Storm supports several types of input:

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

Storm focuses on reachability queries and its support includes

• PCTL and CSL
• Expected Rewards
• Long-run Average Rewards
• Conditional Probabilities
• Multi-objective Model Checking