Verimag

BIP-SMC : A Statistical Model Checking Engine for the BIP framework

BIP-SMC is a Statistical Model Checker, a tool for formal modeling and statistical analysis of systems exhibiting stochastic behaviors.

Models subject to SMC analysis are described in the stochastic BIP language, a component-based formal language. They can have as underlying semantics DTMCs, CTMCs, and GSMPs. Properties to be verified can be specified in Probabilistic Bounded LTL and MTL. In addition to classical SMC algorithms (Hypothesis Testing and Probability Estimation), SBIP provides a parametric exploration (PX) in addition to a recent support for rare events analysis (IP).

 SBIP 2.2.1

The most recent version of SBIP 2.2.1 can be downloaded here (watch the video tutorial on Youtube). Requirements: Ubuntu16.04-64 bits (g++, cmake), Java Runtime Environment (JRE 7), GNU Scientific Libraby (GSL).

A fully configured virtual machine with the tool can be download below (recommended). Follow the instructions in the provided Readme file in the archive.

Virtual machine MD5 checksum
sbip-2.2.1-vm a8f4d6d9d4357a9bee58242015bee536

SBIP is released under CeCILL-B FREE SOFTWARE LICENSE and its source code is available on GitLab.

 Documentation

The tool provides support for DTMCs, CTMCs, GSMPs as input models and for parametric bouded LTL and MTL as properties specifications, in addition to a new support for rare events analysis. See technical report for more information.

The user manual of the tool can be downloaded here and contains installation details and a user guide.

The semantics of the implemented Stochastic Real-Time BIP engine are detailed here.

 Related Case Studies

  • Bluetooth — Device Discovery
  • FireWire — Leader Election
  • Vehicle Gear Controller
  • Precision Time Protocol (PTP)
  • PaceMaker
  • Mutual Exclusion scenario

 Related Publications

[1] Ayoub Nouri, Marius Bozga, Axel Legay, Saddek Bensalem: Performance Evaluation of Complex Systems Using the SBIP Framework. VECoS 2016: 11-26

[2] Ayoub Nouri, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Cyrille Jégourel, Axel Legay: Statistical model checking QoS properties of systems with SBIP. STTT 17(2): 171-185 (2015)

[3] Saddek Bensalem, Marius Bozga, Benoît Delahaye, Cyrille Jégourel, Axel Legay, Ayoub Nouri: Statistical Model Checking QoS Properties of Systems with SBIP. ISoLA (1) 2012: 327-341

 Older Versions

 Related Projects

 Contact

This tool is developed and maintained by:

  • Ayoub Nouri: ayoub.nouri[at]univ-grenoble-alpes.fr
  • Braham Lotfi Mediouni: braham-lotfi.mediouni[at]univ-grenoble-alpes.fr

Contact | Site Map | Site powered by SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 1052875