Plasma Lab main architecture
PLASMA Lab includes three main types of components. A User Interface, a Controler and a set of Plugins.
- Plugins can be of three types: SMC Algorithm, Checker and Simulator. They are loaded by the Controler from a plugins directory at startup.
- The Controler is responsible for the communications between the user (UI or an external tool) and the plugins layer. It provides the methods of our PLASMA Lab API.
- The User Interface is the main entry point of Plasma Lab. It is the standard way of using Plasma Lab, but we also provides a documentation to let you embed Plasma Lab in your program.
PLASMA Lab architecture diagram
Plasma Core and the plugin system
As we can see on the architecture diagram, Plasma Lab uses an interface that we call Plasma Plugins. This is were all the computations are done.
- A Simulator is responsible for executing models and generating traces of these executions.
- A Checker tests the validity of a property on these traces.
- An Algorithm decides if enough tests were made to satisfy the confidence and the precision parameters of the algorithm and in the end computes the results.
Important!
We used the Java Simple Plugin Framework to implement our Plugin System. If you want to use your own Simulator or Checker, please refer to the Plasma Book documentation.
