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.

 SBIP V2

Most recent version (2.0) can be downloaded here (watch the video tutorial on Youtube).

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.0-vm 3b1cbd3c87417d72ab08f455c9275591

Supports for DTMCs, CTMCs, GSMPs as input models and for bouded LTL and MTL as properties specifications.

Requirements: Ubuntu14.04-64 bits (g++, cmake), Java Runtime Environment (JRE 7), GNU Scientific Libraby (GSL).

 Related Case studies

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

 Previous Versions

 Related Case studies

  • MPEG2 Decoder: Buffers sizing vs. delivered video quality
  • CAN/CAN Open: Response time analysis
  • Wireless Sensor Network: Clocks synchronization and buffers sizing
  • Image Recognition on a Many-cores platform: Exec. time analysis

 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

 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 898196