PLASMA Lab uses two types of data, models and requirements. On these pages you will find details on these languages. You could also take at look at our collection of examples.


In its current version, PLASMA Lab is bundled with three model languages:

  • Reactive Module Language (RML) of the PRISM tool, a popular probabilistic model checker tool supporting a wide range of models. More documentation on this language can be found on PRISM website.
  • Adaptive Reactive Module Language is an extension of RML for adaptive systems.
  • Biological Language.

Additionally, three plugins allow to interface PLASMA Lab with external tools:

As we are using a modular architecture, you can also develop your own model language and integrate it into Plasma Lab.


Requirements languages also are modular. Plasma Lab comes with five: