Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Mahieddine Dellabani, Jacques Combaz, Axel Legay and Saddek Bensalem
SBIP 2.0: Statistical Model Checking SRT Systems (2018)
SBIP 2.0: Statistical Model Checking SRT Systems (2018)
TR-2018-5.pdf
Keywords: Stochastic Models, Statistical Analysis, Automated Verification
Abstract: This paper presents a major new release of SBIP, an extensible statistical model checker for Metric (MTL) and Linear-Time Temporal Logic (LTL) properties on respectively Generalized Semi-Markov Processes (GSMP), Continuous-Time (CTMC) and Discrete-Time Markov Chain (DTMC) models. The newly added support for MTL, GSMPs and CTMCs allows to capture both real-time and stochastic aspects, enabling faithful specification and modeling of real-life systems. SBIP was entirely redesigned as an IDE including project management, model edition, compilation, simulation, and statistical analysis. The tool has been used for various benchmarks and case studies including models of communication protocols, embedded and IoT systems.
