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!
Watch the demo tutorial on YouTube!
- MPEG2 Decoder: Buffers sizing vs. delivered video quality
- CAN/CAN Open: Response time analysi
- Wireless Sensor Network: Clocks synchronization and buffers sizing
- Image Recognition on a Many-cores platform: Exec. time analysis
 Ayoub Nouri, Marius Bozga, Axel Legay, Saddek Bensalem: Performance Evaluation of Complex Systems Using the SBIP Framework. VECoS 2016: 11-26
 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)
 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
This tool is developed and maintained by Ayoub Nouri, ayoub.nouri[at]univ-grenoble-alpes.fr