Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Statistical model checking QoS properties of systems with SBIP

  • AD-RV
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Behavior–interaction–priority (BIP) is a component-based framework supporting rigorous design of embedded systems. BIP supports incremental design of large systems from atomic components that communicate via connectors and whose interactions can be described with a powerful algebra. This paper presents SBIP, an extension of BIP for stochastic systems. SBIP offers the possibility to add stochastic information to atomic component’s behaviors, and hence to the entire system. Atomic component’s semantics in SBIP is described by Markov Chains. We show that the semantics of the entire system is described by a Markov chain, showing that the non-determinism arising from system interactions is automatically eliminated by BIP. This allows us to verify systems described in SBIP with Statistical Model Checking. This paper introduces SBIP and illustrates its usability on several industrial case studies.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13

Similar content being viewed by others

References

  1. Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. In: FORTE, vol 6117 of LNCS, pp. 32–46. Springer, Berlin (2010)

  2. Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Sifakis, E.: Verification of an afdx infrastructure using simulations and probabilities. In: Proceedings of the First international conference on Runtime verification, RV’10, pp. 330–344. Springer-Verlag, Berlin, Heidelberg (2010)

  3. Basu, A., Bensalem, S., Gallien, M., Ingrand, F., Lesire, C., Nguyen, T.-H., Sifakis, J.: Incremental component-based construction and verification of a robotic system, In: ECAI (2008)

  4. Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Systems in BIP. In: SEFM06, pp. 3–12, Sep (2006)

  5. Bensalem, S., Bozga, M., Delahaye, B., Jégourel, C., Legay, A., Nouri, A.: Statistical model checking qos properties of systems with sbip. ISoLA 1, 327–341 (2012)

    Google Scholar 

  6. Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-finder: A tool for compositional deadlock detection and verification. In: Proceedings of the 21st International Conference on Computer Aided Verification, CAV ’09, pp. 614–619. Springer-Verlag, Berlin, Heidelberg (2009)

  7. Bensalem, S., Delahaye, B., Legay, A.: Statistical model checking: Present and future. In: RV, vol. 6418 of LNCS. Springer, Berlin (2010)

  8. Bensalem, S., Legay, A., Nouri, A., Peled, D.: Synthesizing distributed scheduling implementation for probabilistic component-based systems. In: MEMOCODE, pp. 87–96 (2013)

  9. Bensalem, S., Silva, L., Griesmayer, A., Ingrand, F., Legay, A., Yan, R.: A formal approach for incremental construction with an application to autonomous robotic systems. In: SC’11, LNCS. Springer, Berlin (2011)

  10. Bip tools. http://www-verimag.imag.fr/BIP-Tools,93.html

  11. Bip2 language. http://www-verimag.imag.fr/TOOLS/DCS/bip/doc/latest/html/

  12. Bliudze, S., Sifakis, J.: The algebra of connectors-structuring interaction in bip. IEEE Trans. Comput. 57(10), 1315–1330 (2008)

    Google Scholar 

  13. Bogdoll, J., Fiorti, L.-M., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: FORTE, LNCS. Springer, Berlin (2011)

  14. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  15. Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems. In: SEFM, pp. 204–220 (2011)

  16. Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Form. Methods Syst. Des. 24(2), 101–127 (2004)

    Article  MATH  Google Scholar 

  17. Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of the 13th International Conference on Computer Aided Verification (CAV’01). Lecture Notes in Computer Science, vol. 2102, pp. 53–65. Springer, Paris (2001)

    Google Scholar 

  18. Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, ASE ’01, pp. 412. IEEE Computer Society, Washington, DC (2001)

  19. Grosu, R., Smolka, S.A.: Monte carlo model checking. In: TACAS, vol. 3440 of LNCS, pp. 271–286. Springer, Berlin (2005)

  20. Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: TACAS, LNCS, pp. 342–356. Springer, Berlin (2002)

  21. Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: VMCAI, pp. 73–84 (2004)

  22. Hoeffding, W.: Probability inequalities. J. Am. Stat. Assoc. 58, 13–30 (1963)

    Article  MATH  MathSciNet  Google Scholar 

  23. Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.S.: How fast and fat is your probabilistic model checker? an experimental performance comparison. In: HVC, vol. 4899 of LNCS. Springer, Berlin (2007)

  24. Jégourel, C., Legay, A., Sedwards, S.: Cross entropy optimisation of importance sampling parameters for statistical model checking. In: CAV (2012)

  25. Jégourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking-plasma. In: TACAS, LNCS, pp. 498–503. Springer, Berlin (2012)

  26. Katoen, J.-P., Zapreev, I.S.: Simulation-based ctmc model checking: an empirical evaluation. In: QEST, pp. 31–40. IEEE Computer Society, Washington, DC (2009)

  27. Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker mrmc. In: QEST, pp. 167–176. IEEE Computer Society, Washington, DC (2009)

  28. Krunz, M., Sass, R., Hughes, H.: Statistical characteristics and multiplexing of MPEG streams. In: INFOCOM, pp. 455–462 (1995)

  29. Krunz, M., Tripathi, S.K.: On the characterization of VBR MPEG streams. In: SIGMETRICS, pp. 192–202 (1997)

  30. Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: QEST, pp. 322–323. IEEE (2004)

  31. Laplante, S., Lassaigne, R., Magniez, F., Peyronnet, S., de Rougemont, M.: Probabilistic abstraction for model checking: an approach based on property testing. ACM TCS 8(4), 20 (2007)

    Article  Google Scholar 

  32. Legay, A., Delahaye, B.: Statistical model checking: an overview. CoRR, abs/1005.1327 (2010)

  33. Nouri, A., Legay, A., Bensalem, S., Bozga, M.: Sbip: a statistical model checking extension for the bip framework. In: First Workshop on Statistical Model Checking (2013)

  34. Parzen, E.: Stochastic Processes. Holden Day, Australia (1962)

    MATH  Google Scholar 

  35. Rabih, D.E., Pekergin, N.: Statistical model checking using perfect simulation. In: ATVA, vol. 5799 of LNCS, pp. 120–134. Springer, Berlin (2009)

  36. Raman, B., Nouri, A., Gangadharan, D., Bozga, M., Basu, A., Maheshwari, M., Legay, A., Bensalem, S., Chakraborty, S.: Stochastic modeling and performance analysis of multimedia socs. In: ICSAMOS, pp. 145–154 (2013)

  37. Rosu, G., Bensalem, S.: Allen linear (interval) temporal logic: translation to ltl and monitor synthesis. In: CAV, vol. 4144 of LNCS, pp. 263–277. Springer, Berlin (2006)

  38. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: CAV, LNCS 3114, pp. 202–215. Springer, Berlin (2004)

  39. Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: CAV, pp. 266–280 (2005)

  40. Vardi, M.Y.: Alternating automata and program verification. In: In Computer Science Today. LNCS 1000, pp. 471–485. Springer-Verlag, Berlin (1995)

  41. Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)

    Article  MATH  MathSciNet  Google Scholar 

  42. Wijesekera, D., Srivastava, J.: Quality of service (QoS) metrics for continuous media. Multimedia Tools Appl. 3(2), 127–166 (1996)

    Article  Google Scholar 

  43. Wolper, P.: Lectures on formal methods and performance analysis. Chapter Constructing automata from temporal logic formulas: a tutorial, pp. 261–277. Springer-Verlag New York Inc, New York (2002)

  44. Ylies, F., Mohamad, J., Thanh-Hung, N., Marius, B., Saddek, B.: Runtime verification of component-based systems in the bip framework with formally-proved sound and complete instrumentation. SOSYM, pp. 1–27 (2013)

  45. Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D thesis, Carnegie Mellon (2005)

  46. Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: SBMF, pp. 144–160 (2010)

  47. Zuliani, P., Baier, C., Clarke, E.M.: Rare-event verification for stochastic hybrid systems. In: HSCC, pp. 217–226. ACM (2012)

  48. Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: HSCC, pp. 243–252. ACM (2010)

Download references

Author information

Authors and Affiliations

  1. UJF-Grenoble 1/CNRS VERIMAG UMR 5104, Grenoble, 38041, France

    Ayoub Nouri, Saddek Bensalem & Marius Bozga

  2. LINA/Université de Nantes, Nantes, France

    Benoit Delahaye

  3. INRIA/IRISA, Rennes, France

    Cyrille Jegourel & Axel Legay

Authors
  1. Ayoub Nouri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Saddek Bensalem
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marius Bozga
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Benoit Delahaye
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Cyrille Jegourel
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Axel Legay.

Additional information

A preliminary version of this paper was published in [5], and the present submission is a special issue extension from [5]. The main differences between [5] and the present paper are: the extension of the background section, a complete description of the stochastic semantic of SBIP (including operational rules), a tutorial on how to use SBIP, and new experimental results. Research supported by the European Community’s Seventh Framework Program [FP7] under grant agreements no. 288175 (CERTAINTY), no. 288917 (DALI), no. 287716 (DANSE), no. 257414 (ASCENS), the ARTEMIS AIPP grant agreement no. 332987 (ARROWHEAD), and Regional CREATIVE project ESTASE.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Nouri, A., Bensalem, S., Bozga, M. et al. Statistical model checking QoS properties of systems with SBIP. Int J Softw Tools Technol Transfer 17, 171–185 (2015). https://doi.org/10.1007/s10009-014-0313-6

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-014-0313-6

Keywords

Search

Navigation