1. Obtain Storm

To be able to run Storm, you need to obtain it and run it on your system. Currently, you can choose one of the following options:

2. Prepare a model checking query

After you have obtained Storm, you need to make sure that your input model has the right form. That is, on a fundamental level, you need to ensure that your input model falls into one of the model types supported by Storm.

If your model indeed does, then the next thing is to have the model available in an input language of Storm. If you don’t have such a model yet, you need to first model the system you are interested in or transcribe it from a different input format.

However, the input model is only “half” of the input you need to provide, the other “half” being the property you want to verify. Please consult our guide to properties for details on how to specify them.

An extensive list of example models and properties is available at the Quantitative Verification Benchmark Set.

3. Run Storm

Finally, if both the input model as well as the property are captured in an appropriate format, then you are ready to run Storm!

Our guide illustrates how you can do so. Since the calls (and even the binaries) you need to invoke depend on the input language for each of the input languages, the guide shows how to run Storm depending on the input you have.