Powered by GitBook

PLASMA Lab book

Architecture

PLASMA Lab has been conceived as a Statistical Model Checking library. The objective is to provide user with a collection of SMC algorithm that they can use with their own tool chain.

The following figure presents a schematic view of PLASMA Lab's design. PLASMA Lab core is in red. This is were the SMC Algorithm library is. Tools use the Controler API, in green, to launch SMC experiment. Simulator and Checker are represented in blue. Thanks to our plugin system, users can integrate their own into PLASMA Lab.

PLASMA Lab tools (PLASMA Lab, PLASMA2Simulink, ...) are using the Controler API to use the SMC library as would an external tool.

MVC Pattern

PLASMA Lab can also be seen as implementing the Model-View-Controler (MVC) pattern. Here, View components use the Controler API to communicate with the Controler component. In turn, the Controler controls the Model components.

In the following section we details which PLASMA Lab project correspond to which type of components and what is their purpose.

View Components

The view is made of several independant project. The main one being the GUI project. Here is a list of view and their associated project.

  • PLASMA Lab Graphical User Interface - fr.inria.plasmalab.ui

This is the main view of PLASMA Lab. It incorporates all functionalities of PLASMA Lab and allows to open and edit PLASMA files (project files).

  • PLASMA Lab Terminal - fr.inria.plasmalab.terminal

This view is a terminal interface for PLASMA Lab which only gives experiment and simulation functionalities.

  • PLASMA Lab Service - fr.inria.plasmalab.service

This view is a graphical or terminal interface for PLASMA Lab distributed service. This is tha part deployed on a distant computer to help run a distributed experiment.

  • PLASMA2Simulink - fr.inria.plasmalab.matlab_UI - plasma_lab_2_simulink

This is a small "App" running from Matlab to use PLASMA Lab SMC algorithms with a Simulink model. The eclipse project (fr.inria.plasmalab.matlab_UI) is a callback interface to the "GUIDE" project (plasma_lab_2_simulink).

Model Components

The Model part contains three type of components. Algorithm, Simulator (Model) and Checker (Requirement/Property). They all are related by a simple workflow. An Algorithm ask a Checker to check a property. The Checker will in turn ask the Simulator to run a simulation and will use the trace returned to decide the property. The decision will be returned to the Algorithm.

Checker and Simulator components are plugins that can be loaded on startup. Algorithms were designed to be plugins too but this feature was discarded. The plugin system use the Java Simple Plugin Framework (JSPF).

The concept behind PLASMA Lab is to provide a SMC Library while end-users can use (and plug-in) there Simulator and Checker.

Here is a list of project for each of these categories.

Algorithm

  • Montecarlo based algorithm - fr.inria.plasmalab.montecarlo
  • Sequential Hypothesis Testing - fr.inria.plasmalab.sequential
  • CUSUM - fr.inria.plasmalab.cusum

Checker

  • Bounded Linear Temporal Logic - fr.inria.plasmalab.bltl
  • Adaptive Linear Temporal Logic - fr.inria.plasmalab.altl
  • Global Contract Specification Language - fr.inria.plasmalab.gcsl

Simulator

  • Reactive Module Language - fr.inria.plasmalab.rmlbis
  • Bio language - fr.inria.plasmalab.bio
  • MatLab interface - fr.inria.plasmalab.matlab
  • CADP interface - fr.inria.plasmalab.caesar

Controler Component

The Controler component (project fr.inria.plasmalab.controler) act as an interface between the Model and the View. The second purpose of the Controler is to initialize PLASMA Lab with configuration files and load plugins.

Note: The project GUI have their own Controler object to deal with file management, interface callback, etc.

Common

Various projects define classes and interfaces used by several component. The main one is the Workflow (project fr.inria.plasmalab.workflow) which contains definition of several interfaces and class as well as a set of PLASMA Lab Exception.

Here is a list of common project

  • Workflow - fr.inria.plasmalab.workflow

Interface and class definitions used by several components, in particular Data and Factory interfaces for Simulator and Checker components. Definitions of PLASMALabException classes.

  • Algorithm - fr.inria.plasmalab.algorithm

Defines Data and Factory interfaces for Algorithm components.

  • Distributed - fr.inria.plasmalab.distributed

Defines the Restlet architecture and components used in all distributed Algorithms as well as a Heartbeat mechanism to detect loss of connection from Workers.