$$\mathcal {S}$$BIP 2.0: Statistical Model Checking Stochastic Real-Time Systems

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