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 | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 873824