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.
Corresponding author; hermanns@cs.utwente.nl, phone: +31 53 489-4661.
Chapter PDF
Similar content being viewed by others
Keywords
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
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.
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.
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.
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.
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.
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.
M. D. Beaudry. Performance-related reliability measures for computing systems. IEEE Transactions on Computers, C-27: 540–547, 1978.
B. Bérard, M. Bidoit, A. Finkel, F. Laroussine, A. Petit, L. Petrucci, and Ph. Schnoebelen. Systems and Software Verification. Springer-Verlag, 2001.
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.
P. Buchholz. Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability, 31: 59–75, 1994.
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.
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.
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.
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.
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.
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
E. Clarke and R. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6): 61–67, 1996.
J. Desharnais and P. Panangaden. Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. Journal of Logic and Algebraic Programming, to appear, 2001.
S. Derisavi, H. Hermanns, and W.H. Sanders. Optimal state space lumping in Markov models. 2002. submitted for publication.
W. Feller. An Introduction to Probability Theory and its Applications. John Wiley & Sons, 1968.
R. German. Performance Analysis of Communication Systems: Modeling with Non-Markovian Stochastic Petri Nets. John Wiley & Sons, 2000.
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.
A. Goyal and A.N. Tantawi. A measure of guaranteed availability and its numerical evaluation. IEEE Transactions on Computers, 37: 25–32, 1988.
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.
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.
D. Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8: 231–274, 1987.
B.R. Haverkort. Performance of Computer Communication Systems: A Model-Based Approach. John Wiley & Sons, 1998.
B.R. Haverkort, R. Marie, G. Rubino, and K.S. Trivedi (editors). Performability Modelling: Techniques and Tools. John Wiley & Sons, 2001.
B.R. Haverkort and I. Niemegeers. Performability modelling tools and techniques. Performance Evaluation, 25: 17–40, 1996.
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.
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.
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.
H. Hermanns. Construction and verfication of performance and reliability models. Bulletin of the EATCS, 74:135–154, 2001.
H. Hermanns, U. Herzog, and J.-P. Katoen. Process algebra for performance evaluation. Theoretical Computer Science, 274(1–2):43–87, 2002.
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.
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.
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.
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.
J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.
G.J. Holzmann. The model checker Spin. IEEE Transactions on Software Engineering, 23(5): 279–295, 1997.
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.
R.A. Howard. Dynamic Probabilistic Systems; Volume 1: Markov Models. John Wiley & Sons, 1971.
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.
A. Jensen. Markov chains as an aid in the study of Markov processes. Skandinavisk Aktuarietidskrift 36: 87–91, 1953.
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.
J.G. Kemeny and J.L. Snell. Finite Markov Chains. Van Nostrand, 1960.
V.G. Kulkarni. Modeling and Analysis of Stochastic Systems. Chapman & Hall, 1995.
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.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
J.F. Meyer. On evaluating the performability of degradable computing systems. IEEE Transactions on Computers, 29(8): 720–731, 1980.
J.F. Meyer. Closed-form solutions of performability, IEEE Transactions on Computers, 31(7): 648–657, 1982.
J.F. Meyer. Performability: a retrospective and some pointers to the future. Performance Evaluation, 14(3–4): 139–156, 1992.
W.D. Obal II and W.H. Sanders. State-space support for path-based reward variables. Performance Evaluation, 35: 233–251, 1999.
D. Peled. Software Reliability Methods. Springer-Verlag, 2001.
W.H. Sanders, W.D. Obal II, M.A. Qureshi, and F.K. Widnajarko. The UltraSAN modeling environment. Performance Evaluation, 24: 89–115, 1995.
B. Sericola. Occupation times in Markov processes. Stochastic Models, 16(5): 339–351, 2000.
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.
W.J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baier, C., Haverkort, B., Hermanns, H., Katoen, JP. (2002). Automated Performance and Dependability Evaluation Using Model Checking. In: Calzarossa, M.C., Tucci, S. (eds) Performance Evaluation of Complex Systems: Techniques and Tools. Performance 2002. Lecture Notes in Computer Science, vol 2459. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45798-4_12
Download citation
DOI: https://doi.org/10.1007/3-540-45798-4_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44252-3
Online ISBN: 978-3-540-45798-5
eBook Packages: Springer Book Archive