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 in BIP.

Models subject to BIP-SMC analysis are described in the stochastic BIP language, a component-based formal language. Properties to be verified are specified in Probabilistic Bounded LTL.


Download and play with the most recent version bip-smc-1.1.1!

Watch the demo tutorial on YouTube!

Older version (bip-smc-1.1) can be found here

 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


This tool is developed and maintained by Ayoub Nouri, ayoub.nouri[at]

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

info visites 874504