PLASMA Lab uses two types of data, models and requirements. Given a model, PLASMA Lab will generate a large number of execution traces and will check the validity of a property for each one of these traces.
On these pages you will find details on these languages. You could also take at look at our examples collection.
Model
In its current version, PLASMA Lab is bundled with three model languages:
- Reactive Module Language (RML) of the PRISM tool, which is a popular probabilistic model checker tool supporting a wide rang of models. More documentation on this language can be found on PRISM web site.
- Adaptive Reactive Module Language is an extension of RML for adaptive systems.
- RML with importance sampling for rare events simulation.
- Biological Language
Additionally, two plugins that can be downloaded from the plugins page allow to interface PLASMA Lab with MATLAB and SystemC:
As we are using a modular architecture, you can develop your own model language and integrate it into Plasma Lab.
Requirements
Requirements languages also are modular. Plasma Lab comes with three:
