SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems

Braham Lotfi Mediouni (1) , Ayoub Nouri (1) , Marius Bozga (1) , Mahieddine Dellabani (1) , Axel Legay (2) , Saddek Bensalem (1)

1 VERIMAG - IMAG - VERIMAG
2 TAMIS - Threat Analysis and Mitigation for Information Security

This paper presents a major new release of SBIP, an extensi-ble 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, CTMCs and rare events allows to capture both real-time and stochastic aspects, allowing faithful specification, modeling and analysis of real-life systems. SBIP is redesigned as an IDE providing project management, model edition, compilation, simulation, and statistical analysis.

Domaines: Systèmes embarqués

Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Mahieddine Dellabani, Axel Legay, et al.. SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems. ATVA 2018 - 16th International Symposium Automated Technology for Verification and Analysis, Oct 2018, Los Angeles, CA, United States. pp.536-542, ⟨10.1007/978-3-030-01090-4_33⟩. ⟨hal-01888538⟩