Advertisement

PLASMA-lab: A Flexible, Distributable Statistical Model Checking Library

  • Benoît Boyer
  • Kevin Corre
  • Axel Legay
  • Sean Sedwards
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)

Abstract

We present PLASMA-lab, a statistical model checking (SMC) library that provides the functionality to create custom statistical model checkers based on arbitrary discrete event modelling languages. PLASMA-lab is written in Java for maximum cross-platform compatibility and has already been incorporated in various performance-critical software and embedded hardware platforms. Users need only implement a few simple methods in a simulator class to take advantage of our efficient SMC algorithms.

PLASMA-lab may be instantiated from the command line or from within other software. We have constructed a graphical user interface (GUI) that exposes the functionality of PLASMA-lab and facilitates its use as a standalone application with multiple ‘drop-in’ modelling languages. The GUI adds the notion of projects and experiments, and implements a simple, practical means of distributing simulations using remote clients.

Keywords

Model Check Graphical User Interface Modelling Language Linear Temporal Logic Simulator Class 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Helbing, D., Molnár, P.: Social force model for pedestrian dynamics. Phys. Rev. E 51, 4282–4286 (1995)CrossRefGoogle Scholar
  2. 2.
    Jegourel, C., Legay, A., Sedwards, S.: A Platform for High Performance Statistical Model Checking – PLASMA. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 498–503. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  3. 3.
    PLASMA-lab project page, https://project.inria.fr/plasma-lab/
  4. 4.
    Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. PhD thesis, Carnegie Mellon University (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Benoît Boyer
    • 1
  • Kevin Corre
    • 1
  • Axel Legay
    • 1
  • Sean Sedwards
    • 1
  1. 1.INRIA Rennes – Bretagne AtlantiqueFrance

Personalised recommendations