Skip to main content
SpringerLink
Log in

Statistical Model Checking: An Overview

  • Conference paper
Runtime Verification (RV 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6418))

Included in the following conference series:

Abstract

Quantitative properties of stochastic systems are usually specified in logics that allow one to compare the measure of executions satisfying certain temporal properties with thresholds. The model checking problem for stochastic systems with respect to such logics is typically solved by a numerical approach [31,8,35,22,21,5] that iteratively computes (or approximates) the exact measure of paths satisfying relevant subformulas; the algorithms themselves depend on the class of systems being analyzed as well as the logic used for specifying the properties. Another approach to solve the model checking problem is to simulate the system for finitely many executions, and use hypothesis testing to infer whether the samples provide a statistical evidence for the satisfaction or violation of the specification. In this tutorial, we survey the statistical approach, and outline its main advantages in terms of efficiency, uniformity, and simplicity.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  2. Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)

    Article  MATH  Google Scholar 

  3. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  4. Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. Technical report, INRIA (2010)

    Google Scholar 

  5. Bustan, D., Rubin, S., Vardi, M.Y.: Verifying omega-regular properties of markov chains. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 189–201. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Carnegie Mellon University. A Bayesian Approach to Model Checking Biological Systems (under submission, 2009)

    Google Scholar 

  7. Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, pp. 131–132. IEEE, Los Alamitos (2006)

    Google Scholar 

  8. Ciesinski, F., Größer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 147–188. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Clarke, E.M., Donzé, A., Legay, A.: Statistical model checking of mixed-analog circuits with an application to a third order delta-sigma modulator. In: HVC 2008. LNCS, vol. 5394, pp. 149–163. Springer, Heidelberg (2008)

    Google Scholar 

  10. Clarke, E.M., Donzé, A., Legay, A.: On simulation-based probabilistic model checking of mixed-analog circuits. Formal Methods in System Design (2009) (to appear)

    Google Scholar 

  11. Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical model checking in biolab: Applications to the automated analysis of t-cell receptor signaling pathway. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 231–250. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Cmacs, http://cmacs.cs.cmu.edu/

  13. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  14. Dang, T., Donze, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid systems techniques. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 21–36. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  15. Faeder, J.R., Blinov, M.L., Hlavacek, W.S.: Graphical rule-based representation of signal-transduction networks. In: SAC 2005: Proceedings of the 2005 ACM symposium on Applied computing, pp. 133–140. ACM, New York (2005)

    Chapter  Google Scholar 

  16. Faeder, J.R., Blinov, M.L., Hlavacek, W.S.: Rule-based modeling of biochemical systems with BioNetGen. In: Maly, I.V. (ed.) Systems Biology. Methods in Molecular Biology. Humana Press, Totowa (2008)

    Google Scholar 

  17. Grosu, R., Smolka, S.A.: Monte carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 271–286. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog designs. In: ICCAD, pp. 210–217 (2004)

    Google Scholar 

  19. Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. Hermanns, H., Wachter, B., Zhang, L.: Probabilistic cegar. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162–175. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Jansen, D.N., Katoen, J., Oldenkamp, M., Stoelinga, M., Zapreev, I.S.: How fast and fat is your probabilistic model checker? an experimental performance comparison. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 69–85. Springer, Heidelberg (2008)

    Google Scholar 

  23. Katoen, J.-P., Zapreev, I.S.: Simulation-based ctmc model checking: An empirical evaluation. In: Proc. of 6th Int. Conference on the Quantitative Evaluation of Systems (QEST), pp. 31–40. IEEE Computer Society, Los Alamitos (2009)

    Google Scholar 

  24. 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: Proc. of 6th Int. Conference on the Quantitative Evaluation of Systems (QEST), pp. 167–176. IEEE Computer Society Press, Los Alamitos (2009)

    Google Scholar 

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

    Google Scholar 

  26. Laplante, S., Lassaigne, R., Magniez, F., Peyronnet, S., de Rougemont, M.: Probabilistic abstraction for model checking: An approach based on property testing. ACM Trans. Comput. Log. 8(4) (2007)

    Google Scholar 

  27. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  28. Merayo, M.G., Hwang, I., Núñez, M., Cavalli, A.R.: A statistical approach to test stochastic and probabilistic systems. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 186–205. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  29. Pnueli, A.: The temporal logic of programs. In: Proc. 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 46–57 (1977)

    Google Scholar 

  30. Rabih, D.E., Pekergin, N.: Statistical model checking using perfect simulation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 120–134. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  31. Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. In: Panangaden, P., van Breugel, F. (eds.) Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.). CRM Monograph Series, vol. 23. American Mathematical Society, Providence (2004)

    Chapter  Google Scholar 

  32. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  33. Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  34. Sen, K., Viswanathan, M., Agha, G.A.: Vesta: A statistical model-checker and analyzer for probabilistic systems. In: QEST, pp. 251–252. IEEE Computer Society, Los Alamitos (2005)

    Google Scholar 

  35. Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327–338 (1985)

    Google Scholar 

  36. Wald, A.: Sequential tests of statistical hypotheses. Annals of Mathematical Statistics 16(2), 117–186 (1945)

    Article  MathSciNet  MATH  Google Scholar 

  37. Younes, H.L.S.: Probabilistic verification for ”black-box” systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 253–265. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Google Scholar 

  39. Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  40. Younes, H.L.S.: Error control for probabilistic model checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 142–156. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  41. Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT 8(3), 216–228 (2006)

    Article  MATH  Google Scholar 

  42. Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  43. Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation 204(9), 1368–1409 (2006)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA/IRISA, Rennes, France

    Axel Legay & Benoît Delahaye

  2. Verimag Laboratory, Université Joseph Fourier Grenoble, CNRS, France

    Saddek Bensalem

Authors
  1. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benoît Delahaye
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Saddek Bensalem
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13 9PL, Manchester, UK

    Howard Barringer

  2. INRIA, Rennes - Bretagne Atlantique, France

    Ylies Falcone

  3. Department of Computer Science, Saarland University, 66123, Saarbrücken, Germany

    Bernd Finkbeiner

  4. Jet Propulsion Laboratory, M/S 3041-285, 4800 Oak Grove Drive, 91109, Pasadena, CA, USA

    Klaus Havelund

  5. PRECISE Center, Department of Computer and Information Science, University of Pennsylvania, 19104, Philadelphia, PA, USA

    Insup Lee  & Oleg Sokolsky  & 

  6. Department of Computer Science, University of Malta, MSD 06, Msida, Malta

    Gordon Pace

  7. Department of Computer Science, University of Illinois at Urbana-Champaign, 201 N. Goodwin, 61801, Urbana, IL, USA

    Grigore Roşu

  8. Microsoft Research,, One Microsoft Way, 98052, Redmond, WA, USA

    Nikolai Tillmann

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Legay, A., Delahaye, B., Bensalem, S. (2010). Statistical Model Checking: An Overview. In: Barringer, H., et al. Runtime Verification. RV 2010. Lecture Notes in Computer Science, vol 6418. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16612-9_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16612-9_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16611-2

  • Online ISBN: 978-3-642-16612-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation