SMC for incomplete models

We have uploaded a new experimental version (1.4.5) of Plasma Lab.
It includes new plugins for analyzing incomplete models (with unknowns):

  • The plugins work with normal RML models that have atomic propositions that may take three values (1 for True, 0 for False, and -1 for Unknown).
  • A new BLTLU plugin allows to check three-valued BLTL properties (same syntax as BLTL).
  • A new Monte-Carlo estimation algorithm for models with unknown.
  • A new hypothesis testing algorithm for models with unknown.
  • The demo examples include an example of an incomplete network model.

PLASMA Lab 1.4.4 Released

A new version of PLASMA Lab (v1.4.4) has been released.

This version adds the following updates:

  • Correction of the distribution mechanism to limit the number of threads created.
  • New option for controlling the frequency of the heartbeat mechanism.
  • Update of the nested BLTL plugin: it now works with a dedicated nested algorithm.

New simulator plugin for LLVM

We have released a new simulator plugin to run LLVM code in PLASMA Lab.

The plugin is a wrapper for the external simulator LODIN developed by the Dependable System Group at the University of Kiel. It allows to run LLVM code with a stochastic semantics, notably to detect race conditions.

The plugin is available on the plugin page and documentation is given on the documentation website. The plugin is distributed in version 1.4.3, the development version of PLASMA Lab, but it can work in the current release 1.4.2.

PLASMA Lab 1.4.2 Released

A new version of PLASMA Lab (v1.4.2) has been released.

This version provides several modifications and new functionalities to PLASMA LAb’s user:

  • Reorganisation and renaming of some SMC algorithms:
    • Merging Monte-Carlo and Chernoff algorithms: the new algorithm interface has 3 parameters, but not all are mandatory. Either “Total sample” is entered; or “Delta” and “Epsilon” and the number of simulations is determined by the Chernoff bound.
    • “Iterated mdp” algorithm is renamed “Smart Sampling”.
    • “Sequential MDP” is renamed “Seq. Smart Sampling”.
  • New comparison algorithm to compare to probabilities.
  • New output format for the command line: “proba” only output a single value (depends on the algorithm, but it usually corresponds to the probability).
  • New format for project files: content (model, requirements, data) can now be a link to a file on the hard drive. This allows to have projects that are easy to use with both the GUI and the CLI. Using the import function of the GUI to add a content from an existing file will use this new format. Creating a new content will use the old format. Old project files are still supported. The demo directory in PLASMA Lab’s bundle uses the new format.

Several modifications concern the developers of  PLASMAS Lab and PLASMA LAb’s plugins:

  • New AbstractClasses in the API  that implements common functions of algorithm, scheduler and workers.
  • Updating the distribution mechanism: workers are properly stopped which facilitates scripting of PLASMA Lab Service.
  • Updating Plasma Lab exceptions.

Plasma Lab Tutorial

We gave a tutorial on Plasma Lab at the last SOFSEM conference in Limerick. The slides are available here.

We presented the architecture of Plasma Lab, its usage and how the tool can be extended with new plugins. A post-proceedings paper on this tutorial should follow soon.


PLASMA Lab 1.4.0 Released

A new version of PLASMA Lab (v1.4.0) has been released.

  • This version makes some important changes on the structure of PLASMA Lab. Old versions of the plugins may not be compatible.
  • It provides a new command line interface with more capabilities.
  • It provides a new cross-entropy minimization algorithm for rare events simulation with importance sampling.
  • The online documentation has been moved to a dedicated website.

PLASMA Lab 1.3.8 Released

A new version of PLASMA Lab (v1.3.8) has been released.
This version improves the importance splitting algorithm:

  • Better performances.
  • Improvement of the results display.
  • A bug with the observers has been fixed.

PLASMA Lab 1.3.6 Released

A new version of PLASMA Lab (v1.3.6) has been released.
This version introduces several corrections:

  • The CUSUM algorithm has been corrected.
  • The CUSUM interface now provides three different checks: one for the classical CUSUM algorithm, one for simulating the algorithm in order to estimate the stopping rule, and one that applies Monte Carlo analyses along a trace to check the independence between delayed samples.
  • The BLTL plugin has been corrected . There was a possible bug when checking some nested properties and the weak until operator is now operational.