Accueil > Verimag > Outils

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

Sommaire

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.3

The most recent version of SBIP 2.2.3 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.3-vm	4a6e8ad6b98c628081889f1b0c078395

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] Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Mahieddine Dellabani, Axel Legay and Saddek Bensalem : SBIP 2.0 : Statistical Model Checking Stochastic Real-time Systems. ATVA 2018

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

[3] 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)

[4] 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