Advertisement

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

  • Braham Lotfi MediouniEmail author
  • Ayoub Nouri
  • Marius Bozga
  • Mahieddine Dellabani
  • Axel Legay
  • Saddek Bensalem
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

Abstract

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.

References

  1. 1.
    Ballarini, P., Barbot, B., Duflot, M., Haddad, S., Pekergin, N.: Hasl: a new approach for performance evaluation and model checking from concepts to experimentation. Perform. Eval. 90, 53–77 (2015)CrossRefGoogle Scholar
  2. 2.
    Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011)CrossRefGoogle Scholar
  3. 3.
    Bulychev, P.E., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. RV, 7687, 260–275 (2012)Google Scholar
  4. 4.
    David, A., Larsen, K.G., Legay, A., Mikuăionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397–415 (2015)CrossRefGoogle Scholar
  5. 5.
    Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24622-0_8CrossRefzbMATHGoogle Scholar
  6. 6.
    Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking – PLASMA. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 498–503. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28756-5_37CrossRefzbMATHGoogle Scholar
  7. 7.
    Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576–591. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_38CrossRefGoogle Scholar
  8. 8.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  9. 9.
    Nouri, A., Bensalem, S., Bozga, M., Delahaye, B., Jegourel, C., Legay, A.: Statistical model checking QoS properties of systems with SBIP. In: STTT 2015, vol. 17, pp. 171–185CrossRefGoogle Scholar
  10. 10.
    Nouri, A., Mediouni, B.L., Bozga, M., Combaz, J., Legay, A., Bensalem, S.: Performance evaluation of stochastic real-time systems with the SBIP framework. Technical Report TR-2017-6, Verimag Research Report (2017)Google Scholar
  11. 11.
    Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151–197 (2005)CrossRefGoogle Scholar
  12. 12.
    Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon (2005)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Braham Lotfi Mediouni
    • 1
    Email author
  • Ayoub Nouri
    • 1
  • Marius Bozga
    • 1
  • Mahieddine Dellabani
    • 1
  • Axel Legay
    • 2
  • Saddek Bensalem
    • 1
  1. 1.Univ. Grenoble Alpes, CNRS, Grenoble INP*, VERIMAGGrenobleFrance
  2. 2.INRIARennesFrance

Personalised recommendations