Skip to main content
SpringerLink
Log in

Probabilistic Verification at Runtime for Self-Adaptive Systems

  • Chapter
Assurances for Self-Adaptive Systems

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

Abstract

An effective design of effective and efficient self-adaptive systems may rely on several existing approaches. Software models and model checking techniques at run time represent one of them since they support automatic reasoning about such changes, detect harmful configurations, and potentially enable appropriate (self-)reactions. However, traditional model checking techniques and tools may not be applied as they are at run time, since they hardly meet the constraints imposed by on-the-fly analysis, in terms of execution time and memory occupation. For this reason, efficient run-time model checking represents a crucial research challenge.

This paper precisely addresses this issue and focuses on probabilistic run-time model checking in which reliability models are given in terms of Discrete Time Markov Chains which are verified at run-time against a set of requirements expressed as logical formulae. In particular, the paper discusses the use of probabilistic model checking at run-time for self-adaptive systems by surveying and comparing the existing approaches divided in two categories: state-elimination algorithms and algebra-based algorithms. The discussion is supported by a realistic example and by empirical experiments.

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

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.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. Andova, S., Hermanns, H., Katoen, J.P.: Discrete-time rewards model-checked. Formal Modeling and Analysis of Timed Systems, 88–104 (2004)

    Google Scholar 

  2. Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: It usually works: The temporal logic of stochastic systems. In: Computer Aided Verification, pp. 155–165. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  3. Baier, C., D’Argenio, P., Groesser, M.: Partial order reduction for probabilistic branching time. Electronic Notes in Theoretical Computer Science 153(2), 97–116 (2006)

    Article  Google Scholar 

  4. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Transactions on Software Engineering 29, 524–541 (2003)

    Article  MATH  Google Scholar 

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

    MATH  Google Scholar 

  6. Baresi, L., Di Nitto, E., Ghezzi, C.: Toward open-world software: Issue and challenges. Computer 39(10), 36–43 (2006)

    Article  Google Scholar 

  7. Calinescu, R., Grunske, L., Kwiatkowska, M., Mirandola, R., Tamburrelli, G.: Dynamic qos management and optimisation in service-based systems. IEEE Transactions on Software Engineering (99), 1 (2010)

    Google Scholar 

  8. Cheung, R.C.: A user-oriented software reliability model. IEEE Trans. Softw. Eng. 6(2), 118–125 (1980)

    Article  MATH  Google Scholar 

  9. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4) (1995)

    Google Scholar 

  10. Davis, T.A.: Direct methods for sparse linear systems. Society for Industrial Mathematics, vol. 2 (2006)

    Google Scholar 

  11. Daws, C.: Symbolic and parametric model checking of discrete-time markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280–294. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: 33rd International Conference on Software Engineering (ICSE 2011) (accepted for publication)

    Google Scholar 

  13. Antonio Filieri and Carlo Ghezzi. Further steps towards efficient runtime verification: Handling probabilistic cost models. In Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA), Zurich, 2012.

    Google Scholar 

  14. Goseva-Popstojanova, K., Trivedi, K.S.: Architecture-based approach to reliability assessment of software systems. Performance Evaluation 45(2-3), 179–204 (2001)

    Article  MATH  Google Scholar 

  15. Grinstead, C.M., Snell, J.L.: Introduction to Probability. Amer Mathematical Society (1997)

    Google Scholar 

  16. Gruber, H., Johannsen, J.: Optimal Lower Bounds on Regular Expression Size Using Communication Complexity. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 273–286. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Grunske, L.: Specification patterns for probabilistic quality properties. In: ICSE, pp. 31–40 (2008)

    Google Scholar 

  18. Hahn, E., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric markov models. In: Model Checking Software, pp. 88–106 (2009)

    Google Scholar 

  19. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal aspects of computing 6(5), 512–535 (1994)

    Article  MATH  Google Scholar 

  20. Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation. Addison-Wesley (2007)

    Google Scholar 

  21. Immonen, A., Niemelä, E.: Survey of reliability and availability prediction methods from the viewpoint of software architecture. Software and Systems Modeling 7(1), 49–65 (2008)

    Article  Google Scholar 

  22. Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.: 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)

    Chapter  Google Scholar 

  23. Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Kramer, J., Magee, J.: Self-managed systems: An architectural challenge. In: Future of Software Engineering, FOSE 2007, pp. 259–268. IEEE (2007)

    Google Scholar 

  25. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic Model Checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Kwiatkowska, M.Z., Parker, D., Qu, H.: Incremental quantitative verification for markov decision processes. In: DSN, pp. 359–370 (2011)

    Google Scholar 

  27. Caporuscio, M., Funaro, M., Ghezzi, C.: Architectural Issues of Adaptive Pervasive Systems. In: Engels, G., Lewerentz, C., Schäfer, W., Schürr, A., Westfechtel, B. (eds.) Nagl Festschrift. LNCS, vol. 5765, pp. 492–511. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  28. Quarteroni, A., Sacco, R., Saleri, F.: Numerical mathematics, vol. 37. Springer (2007)

    Google Scholar 

  29. Ross, S.M.: Stochastic Processes. Wiley, New York (1996)

    MATH  Google Scholar 

  30. Saad, Y.: Iterative methods for sparse linear systems. Society for Industrial Mathematics (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DeepSE Group @ DEI, Politecnico di Milano, Italy

    Antonio Filieri & Giordano Tamburrelli

Authors
  1. Antonio Filieri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Giordano Tamburrelli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics Engineering, University of Coimbra, 3030-290, Coimbra, Portugal

    Javier Cámara

  2. School of Computing, University of Kent, CT2 7NF, Canterbury, Kent, UK

    Rogério de Lemos

  3. Dipartimento di Elettronica e Informazione, Politecnico di Milano, Via Golgi, 42, 20133, Milano, Italy

    Carlo Ghezzi

  4. Faculty of Sciences, University of Lisbon, Campo Grande, 1749-016, Portugal

    Antónia Lopes

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Filieri, A., Tamburrelli, G. (2013). Probabilistic Verification at Runtime for Self-Adaptive Systems. In: Cámara, J., de Lemos, R., Ghezzi, C., Lopes, A. (eds) Assurances for Self-Adaptive Systems. Lecture Notes in Computer Science, vol 7740. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36249-1_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-36249-1_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-36248-4

  • Online ISBN: 978-3-642-36249-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation