Advertisement

Automated Performance and Dependability Evaluation Using Model Checking

  • Christel Baier
  • Boudewijn Haverkort
  • Holger Hermanns
  • Joost-Pieter Katoen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2459)

Abstract

Markov chains (and their extensions with rewards) have been widely used to determine performance, dependability and performability characteristics of computer communication systems, such as throughput, delay, mean time to failure, or the probability to accumulate at least a certain amount of reward in a given time.

Due to the rapidly increasing size and complexity of systems, Markov chains and Markov reward models are difficult and cumbersome to specify by hand at the state-space level. Therefore, various specification formalisms, such as stochastic Petri nets and stochastic process algebras, have been developed to facilitate the specification of these models at a higher level of abstraction. Uptill now, however, the specification of the measure-of-interest is often done in an informal and relatively unstructured way. Furthermore, some measures-of-interest can not be expressed conveniently at all.

In this tutorial paper, we present a logic-based specification technique to specify performance, dependability and performability measures-ofinterest and show how for a given finite Markov chain (or Markov reward model) such measures can be evaluated in a fully automated way. Particular emphasis will be given to so-called path-based measures and hierarchically-specified measures. For this purpose, we extend so-called model checking techniques to reason about discrete- and continuous-time Markov chains and their rewards.We also report on the use of techniques such as (compositional) model reduction and measure-driven state-space generation to combat the infamous state space explosion problem.

Keywords

Model Check Dependability Evaluation Atomic Proposition Reward Structure Model Check Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model checking continuous time Markov chains. ACM Transactions on Computational Logic, 1(1): 162–170, 2000.CrossRefMathSciNetGoogle Scholar
  2. 2.
    C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In Concurrency Theory, LNCS 1664: 146–162, Springer-Verlag, 1999.CrossRefGoogle Scholar
  3. 3.
    C. Baier, B.R. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In Computer Aided Verification, LNCS 1855: 358–372, Springer-Verlag, 2000.CrossRefGoogle Scholar
  4. 4.
    C. Baier, B.R. Haverkort, H. Hermanns, and J.-P. Katoen. On the logical characterisation of performability properties. In Automata, Languages, and Programming, LNCS 1853: 780–792, Springer-Verlag, 2000.CrossRefGoogle Scholar
  5. 5.
    C. Baier, B.R. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking algorithms for continuous-time Markov chains. Technical report TR-CTIT-02-10. Centre for Telematics and Information Technology, University of Twente. 2001.Google Scholar
  6. 6.
    C. Baier and M. Kwiatkowska. On the verification of qualitative properties of probabilistic processes under fairness constraints. Information Processing Letters, 66(2): 71–79, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    M. D. Beaudry. Performance-related reliability measures for computing systems. IEEE Transactions on Computers, C-27: 540–547, 1978.CrossRefGoogle Scholar
  8. 8.
    B. Bérard, M. Bidoit, A. Finkel, F. Laroussine, A. Petit, L. Petrucci, and Ph. Schnoebelen. Systems and Software Verification. Springer-Verlag, 2001.Google Scholar
  9. 9.
    A. Bobbio and M. Telek. Markov regenerative SPN with non-overlapping activity cycles. In Proc. Int’l IEEE Performance and Dependability Symposium: 124–133, 1995.Google Scholar
  10. 10.
    P. Buchholz. Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability, 31: 59–75, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    P. Buchholz, J.-P. Katoen, P. Kemper, and C. Tepper. Model checking large structured Markov chains. Journal of Logic and Algebraic Programming, to appear, 2001.Google Scholar
  12. 13.
    G. Chiola, G. Franceschinis, R. Gaeta, and M. Ribaudo. GreatSPN 1.7: graphical editor and analyzer for timed and stochastic Petri nets. Performance Evaluation, 24(1–2):47–68, 1995.zbMATHCrossRefGoogle Scholar
  13. 14.
    G. Ciardo, J.K. Muppala, and K.S. Trivedi. SPNP: stochastic Petri net package. In Proc. 3rd Int. Workshop on Petri Nets and Performance Models, pp. 142–151, IEEE CS Press, 1989.Google Scholar
  14. 15.
    G. Clark, S. Gilmore, and J. Hillston. Specifying performance measures for PEPA. In Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601: 211–227, Springer-Verlag, 1999.CrossRefGoogle Scholar
  15. 16.
    E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8: 244–263, 1986.zbMATHCrossRefGoogle Scholar
  16. 17.
    E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.Google Scholar
  17. 18.
    E. Clarke and R. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6): 61–67, 1996.CrossRefGoogle Scholar
  18. 19.
    J. Desharnais and P. Panangaden. Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. Journal of Logic and Algebraic Programming, to appear, 2001.Google Scholar
  19. 20.
    S. Derisavi, H. Hermanns, and W.H. Sanders. Optimal state space lumping in Markov models. 2002. submitted for publication.Google Scholar
  20. 21.
    W. Feller. An Introduction to Probability Theory and its Applications. John Wiley & Sons, 1968.Google Scholar
  21. 22.
    R. German. Performance Analysis of Communication Systems: Modeling with Non-Markovian Stochastic Petri Nets. John Wiley & Sons, 2000.Google Scholar
  22. 23.
    S. Gilmore and J. Hillston. The PEPA workbench: a tool to support a process algebra-based approach to performance modelling. In Computer Performance Evaluation, Modeling Techniques and Tools, LNCS 794: 353–368, Springer-Verlag, 1994.Google Scholar
  23. 24.
    A. Goyal and A.N. Tantawi. A measure of guaranteed availability and its numerical evaluation. IEEE Transactions on Computers, 37: 25–32, 1988.CrossRefGoogle Scholar
  24. 25.
    W.K. Grassmann. Finding transient solutions in Markovian event systems through randomization. In Numerical Solution of Markov Chains, pp. 357–371, Marcel Dekker Inc, 1991.Google Scholar
  25. 26.
    D. Gross and D.R. Miller. The randomization technique as a modeling tool and solution procedure for transient Markov chains. Operations Research 32(2): 343–361, 1984.zbMATHMathSciNetCrossRefGoogle Scholar
  26. 27.
    D. Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8: 231–274, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  27. 28.
    B.R. Haverkort. Performance of Computer Communication Systems: A Model-Based Approach. John Wiley & Sons, 1998.Google Scholar
  28. 29.
    B.R. Haverkort, R. Marie, G. Rubino, and K.S. Trivedi (editors). Performability Modelling: Techniques and Tools. John Wiley & Sons, 2001.Google Scholar
  29. 30.
    B.R. Haverkort and I. Niemegeers. Performability modelling tools and techniques. Performance Evaluation, 25: 17–40, 1996.zbMATHCrossRefGoogle Scholar
  30. 31.
    B.R. Haverkort, H. Hermanns, and J.-P. Katoen. The use of model checking techniques for quantitative dependability evaluation. In IEEE Symposium on Reliable Distributed Systems., pp. 228–238. IEEE CS Press, 2000.Google Scholar
  31. 32.
    B.R. Haverkort, L. Cloth, H. Hermanns, J.-P. Katoen, and C. Baier. Model checking CSRL-specified performability properties. In 5th Int. Workshop on Performability Modeling of Computer and Communication Systems, Erlangen, Arbeitsberichte des IMMD, 34 (13), 2001. 2001.Google Scholar
  32. 33.
    B.R. Haverkort, L. Cloth, H. Hermanns, J.-P. Katoen, and C. Baier. Model checking performability properties. In Proc. IEEE Int’l Conference on Dependable Systems and Networks, IEEE CS press, 2002.Google Scholar
  33. 34.
    H. Hermanns. Construction and verfication of performance and reliability models. Bulletin of the EATCS, 74:135–154, 2001.zbMATHMathSciNetGoogle Scholar
  34. 35.
    H. Hermanns, U. Herzog, and J.-P. Katoen. Process algebra for performance evaluation. Theoretical Computer Science, 274(1–2):43–87, 2002.zbMATHCrossRefMathSciNetGoogle Scholar
  35. 36.
    H. Hermanns, U. Herzog, U. Klehmet, V. Mertsiotakis, and M. Siegle. Compositional performance modelling with the TIPPtool. Performance Evaluation, 39(1–4): 5–35, 2000.zbMATHCrossRefGoogle Scholar
  36. 37.
    H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov chain model checker. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1785: 347–362, Springer-Verlag, 2000.CrossRefGoogle Scholar
  37. 38.
    H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. Towards model checking stochastic process algebra. In Integrated Formal Methods, LNCS 1945: 420–439, Springer-Verlag, 2000.CrossRefGoogle Scholar
  38. 39.
    H. Hermanns and M. Siegle. Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601: 244–265, Springer-Verlag, 1999.CrossRefGoogle Scholar
  39. 40.
    J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.Google Scholar
  40. 41.
    G.J. Holzmann. The model checker Spin. IEEE Transactions on Software Engineering, 23(5): 279–295, 1997.CrossRefMathSciNetGoogle Scholar
  41. 42.
    G. Horton, V. Kulkarni, D. Nicol, K. Trivedi. Fluid stochastic Petri nets: Theory, application and solution techniques. Eur. J. Oper. Res., 105(1): 184–201,1998.zbMATHCrossRefGoogle Scholar
  42. 43.
    R.A. Howard. Dynamic Probabilistic Systems; Volume 1: Markov Models. John Wiley & Sons, 1971.Google Scholar
  43. 44.
    G.G. Infante-Lopez, H. Hermanns, and J.-P. Katoen. Beyond memoryless distributions: Model checking semi-Markov chains. In Process Algebra and Probabilistic Methods, LNCS 2165: 57–70, Springer-Verlag, 2001.Google Scholar
  44. 45.
    A. Jensen. Markov chains as an aid in the study of Markov processes. Skandinavisk Aktuarietidskrift 36: 87–91, 1953.Google Scholar
  45. 46.
    J.-P. Katoen, M.Z. Kwiatkowska, G. Norman, and D. Parker. Faster and symbolic CTMC model checking. In Process Algebra and Probabilistic Methods, LNCS 2165: 23–38, Springer-Verlag, 2001.Google Scholar
  46. 47.
    J.G. Kemeny and J.L. Snell. Finite Markov Chains. Van Nostrand, 1960.Google Scholar
  47. 48.
    V.G. Kulkarni. Modeling and Analysis of Stochastic Systems. Chapman & Hall, 1995.Google Scholar
  48. 49.
    M.Z. Kwiatkowska, G. Norman, and A. Pacheco. Model checking CSL until formulae with random time bounds. In Process Algebra and Probabilistic Methods, LNCS 2399, Springer-Verlag, 2002.Google Scholar
  49. 50.
    K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  50. 51.
    J.F. Meyer. On evaluating the performability of degradable computing systems. IEEE Transactions on Computers, 29(8): 720–731, 1980.zbMATHCrossRefGoogle Scholar
  51. 52.
    J.F. Meyer. Closed-form solutions of performability, IEEE Transactions on Computers, 31(7): 648–657, 1982.CrossRefGoogle Scholar
  52. 53.
    J.F. Meyer. Performability: a retrospective and some pointers to the future. Performance Evaluation, 14(3–4): 139–156, 1992.CrossRefzbMATHGoogle Scholar
  53. 54.
    W.D. Obal II and W.H. Sanders. State-space support for path-based reward variables. Performance Evaluation, 35: 233–251, 1999.zbMATHCrossRefGoogle Scholar
  54. 55.
    D. Peled. Software Reliability Methods. Springer-Verlag, 2001.Google Scholar
  55. 56.
    W.H. Sanders, W.D. Obal II, M.A. Qureshi, and F.K. Widnajarko. The UltraSAN modeling environment. Performance Evaluation, 24: 89–115, 1995.zbMATHCrossRefGoogle Scholar
  56. 57.
    B. Sericola. Occupation times in Markov processes. Stochastic Models, 16(5): 339–351, 2000.MathSciNetCrossRefGoogle Scholar
  57. 58.
    E. de Souza e Silva and H.R. Gail. Performability analysis of computer systems: from model specification to solution. Perf. Ev., 14: 157–196, 1992.CrossRefzbMATHGoogle Scholar
  58. 59.
    W.J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994.Google Scholar
  59. 60.
    H.C. Tijms, R. Veldman. A fast algorithm for the transient reward distribution in continuous-time Markov chains, Operation Research Letters, 26: 155–158, 2000.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Christel Baier
    • 1
  • Boudewijn Haverkort
    • 2
  • Holger Hermanns
    • 3
  • Joost-Pieter Katoen
    • 3
  1. 1.Institut für Informatik IUniversity of BonnBonnGermany
  2. 2.Dept. of Computer ScienceRWTH AachenAachenGermany
  3. 3.Faculty of Computer ScienceUniversity of TwenteAE EnschedeThe Netherlands

Personalised recommendations