Plasma Lab Statistical Model Checker: Architecture, Usage and Extension

International audiencePlasma Lab is a modular statistical model checking (SMC) platform that facilitates multiple SMC algorithms and multiple modelling and query languages. Plasma Lab may be used as a stand-alone tool with a graphical development environment or invoked from the command line for high performance scripting applications. This tutorial first presents an overview of Plasma Lab architecture, modelling languages and algorithms. Then we present the usage of the tool to design models and perform various experiments Finally we propose a tutorial on how to develop a new plugin for Plasma Lab