Hostname: page-component-55f67697df-twqc4 Total loading time: 0 Render date: 2025-05-12T21:04:12.376Z Has data issue: false hasContentIssue false

Model checking for performability

Published online by Cambridge University Press: 08 July 2013

C. BAIER
Affiliation:
Technische Universität Dresden, Dresden, Germany Email: baier@tcs.inf.tu-dresden.de
E. M. HAHN
Affiliation:
Saarland University, Saarbrücken, Germany Email: hermanns@cs.uni-saarland.de; emh@cs.uni-saarland.de
B. R. HAVERKORT
Affiliation:
Embedded Systems Institute, Eindhoven, The Netherlands and University of Twente, Enschede, The Netherlands Email: brh@cs.utwente.nl
H. HERMANNS
Affiliation:
Saarland University, Saarbrücken, Germany Email: hermanns@cs.uni-saarland.de; emh@cs.uni-saarland.de
J.-P. KATOEN
Affiliation:
University of Twente, Enschede, The Netherlands and RWTH Aachen University, Aachen, Germany Email: katoen@cs.rwth-aachen.de

Abstract

This paper gives a bird's-eye view of the various ingredients that make up a modern, model-checking-based approach to performability evaluation: Markov reward models, temporal logics and continuous stochastic logic, model-checking algorithms, bisimulation and the handling of non-determinism. A short historical account as well as a large case study complete this picture. In this way, we show convincingly that the smart combination of performability evaluation with stochastic model-checking techniques, developed over the last decade, provides a powerful and unified method of performability evaluation, thereby combining the advantages of earlier approaches.

Type
Paper
Copyright
Copyright © Cambridge University Press 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

References

Abate,A.,Katoen,J.-P. andMereacre,A. (2011)Quantitative automata model checking of autonomous stochastic hybrid systems. In:Hybrid Systems: Computation and Control (HSCC),ACM83–92.Google Scholar
Abate,A.,Prandini,M.,Lygeros,J. andSastry,S. (2008)Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems.Automatica44(11)2724–2734.CrossRefGoogle Scholar
Ajmone Marsan,M.,Conte,G. andBalbo,G. (1984)A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems.ACM Transactions on Computer Systems293–122.CrossRefGoogle Scholar
Aldini,A. andBernardo,M. (2007)Mixing logics and rewards for the component-oriented specification of performance measures.Theoretical Computer Science3823–23.CrossRefGoogle Scholar
Arnold,T. (1973)The concept of coverage and its effect on the reliability model of a repairable system.IEEE Transactions on Computers22251–254.CrossRefGoogle Scholar
Avizienis,A.,Laprie,J.-C.,Randell,B. andLandwehr,C. E. (2004)Basic concepts and taxonomy of dependable and secure computing.IEEE Transactions on Dependable and Secure Computing1(1)11–33.CrossRefGoogle Scholar
Aziz,A.,Sanwal,K.,Singhal,V. andBrayton,R. K. (2000)Model-checking continuous-time Markov chains.ACM Transactions on Computational Logic1(1)162–170.CrossRefGoogle Scholar
Baier,C.,Cloth,L.,Haverkort,B. R.,Hermanns,H. andKatoen,J.-P. (2010a)Performability assessment by model checking of Markov reward models.Formal Methods in System Design36(1)1–36.CrossRefGoogle Scholar
Baier,C.,Haverkort,B. R.,Hermanns,H. andKatoen,J. (2000)On the logical characterisation of performability properties. In: International Colloquium on Automata, Languages, and Programming (ICALP).Springer-Verlag Lecture Notes in Computer Science1853780–792.CrossRefGoogle Scholar
Baier,C.,Haverkort,B. R.,Hermanns,H. andKatoen,J.-P. (2003)Model-checking algorithms for continuous-time Markov chains.IEEE Transactions on Software Engineering29524–541.CrossRefGoogle Scholar
Baier,C.,Haverkort,B. R.,Hermanns,H. andKatoen,J.-P. (2008)Reachability in continuous-time Markov reward decision processes. In:Flum,J.,Grädel,E. andWilke,T. (eds.)Logic and Automata, Texts in Logic and Games2,Amsterdam University Press53–72.Google Scholar
Baier,C.,Haverkort,B. R.,Hermanns,H. andKatoen,J.-P. (2010b)Performance evaluation and model checking join forces.Communications of the ACM5376–85.CrossRefGoogle Scholar
Baier,C. andHermanns,H. (1997)Weak bisimulation for fully probabilistic processes. In: Computer Aided Verification (CAV).Springer-Verlag Lecture Notes in Computer Science1254119–130.CrossRefGoogle Scholar
Baier,C.,Hermanns,H.,Katoen,J.-P. andHaverkort,B. R. (2005a)Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes.Theoretical Computer Science345(1)2–26.CrossRefGoogle Scholar
Baier,C. andKatoen,J.-P. (2008)Principles of Model Checking,MIT Press.Google Scholar
Baier,C.,Katoen,J.-P. andHermanns,H. (1999)Approximate symbolic model checking of continuous-time Markov chains. In: Concurrency Theory (CONCUR).Springer-Verlag Lecture Notes in Computer Science1664146–161.CrossRefGoogle Scholar
Baier,C.,Katoen,J.-P.,Hermanns,H. andWolf,V. (2005b)Comparative branching-time semantics for Markov chains.Information and Computation200(2)149–214.CrossRefGoogle Scholar
Beaudry,M. (1978)Performance-related reliability measures for computing systems.IEEE Transactions on Computer Systems27(6)540–547.CrossRefGoogle Scholar
Berendsen,J.,Jansen,D. N. andKatoen,J.-P. (2006)Probably on time and within budget: On reachability in priced probabilistic timed automata. In:Quantitative Evaluation of Systems (QEST),IEEE Computer Society Press311–322.Google Scholar
Bernardo,M. andBravetti,M. (2001)Reward based congruences: Can we aggregate more? In: Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV).Springer-Verlag Lecture Notes in Computer Science2165136–151.CrossRefGoogle Scholar
Brázdil,T.,Forejt,V.,Krčál,J.,Křetínský,J., andKučera,A. (2009)Continuous-time stochastic games with time-bounded reachability. In: FSTTCS.LIPIcs4, Schloss Dagstuhl61–72.Google Scholar
Buchholz,P.,Hahn,E. M.,Hermanns,H. andZhang,L. (2011)Model checking algorithms for CTMDPs. In: CAV.Springer-Verlag Lecture Notes in Computer Science6806225–242.CrossRefGoogle Scholar
Caillaud,B.,Delahaye,B.,Larsen,K.,Legay,A.,Pedersen,M. andWasowski,A. (2010)Compositional design methodology with constraint Markov chains. In:Quantitative Evaluation of Systems (QEST),IEEE Computer Society Press123–132.Google Scholar
Chiola,G. (1985)A software package of the analysis of generalized stochastic Petri nets. In:Proceedings of the 1st International Workshop on Timed Petri Nets,IEEE Computer Society Press136–143.Google Scholar
Ciardo,G.,Jones,R. L.III,Miner,A. S. andSiminiceanu,R. (2003)Logical and stochastic modeling with SMART. In: Computer Performance Evaluation/TOOLS.Springer-Verlag Lecture Notes in Computer Science279478–97.CrossRefGoogle Scholar
Ciardo,G.,Miner,A. S.,Wan,M. andYu,A. J. (2007)Approximating stationary measures of structured continuous-time Markov models using matrix diagrams.ACM SIGMETRICS Performance Evaluation Review35(3)16–18.CrossRefGoogle Scholar
Clarke,E. M.,Emerson,E. A. andSistla,A. P. (1986)Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems8244–263.CrossRefGoogle Scholar
Cloth,L. andHaverkort,B. R. (2005)Model checking for survivability! In:Quantitative Evaluation of Systems (QEST),IEEE Computer Society145–154.Google Scholar
Cloth,L.,Jongerden,M. R. andHaverkort,B. R. (2007)Computing battery lifetime distributions. In:Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN),IEEE Computer Society780–789.Google Scholar
Desharnais,J. andPanangaden,P. (2003)Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.Journal of Logic and Algebraic Programming56(1–2)99–115.CrossRefGoogle Scholar
Donatiello,L. andIyer,B. (1987a)Analysis of a composite performance reliability measure for fault-tolerant systems.Journal of the ACM34(1)179–199.CrossRefGoogle Scholar
Donatiello,L. andIyer,B. (1987b)Closed-form solution for system availability.IEEE Transactions on Reliability36(1)45–47.CrossRefGoogle Scholar
Furchtgott,D. andMeyer,J. F. (1984)A performability solution method for degradable non-repairable systems.IEEE Transactions on Computers33(6)550–554.CrossRefGoogle Scholar
Gay,F. A. andKetelsen,M. L. (1979)Performance evaluation for gracefully degrading systems. In:Proceedings of the 9th Fault-Tolerant Computer Systems Systems (FTCS),IEEE Computer Society Press51–58.Google Scholar
Geist,R. andTrivedi,K. S. (1990)Reliability estimation of fault-tolerant systems: Tools and techniques.Computer23(7)52–61.CrossRefGoogle Scholar
Ghemawat,S.,Gobioff,H. andLeung,S.-T. (2003)The Google file system. In:ACM Symposium on Operating Systems Principles (SOSP),ACM29–43.CrossRefGoogle Scholar
Goyal,A.,Lavenberg,S. andTrivedi,K. S. (1987)The system availability estimator.Annals of Operations Research8285–306.CrossRefGoogle Scholar
Goyal,A. andTantawi,A. (1988)A measure of guaranteed availability and its numerical evaluation.IEEE Transactions on Computers37(1)25–32.CrossRefGoogle Scholar
Goyal,A. andTantawi,A. N. (1987)Evaluation of performability for degradable computer systems.IEEE Transactions on Computers36(6)7.Google Scholar
Grassi,V.,Donatiello,L. andIazeolla,G. (1988)Performability evaluation of multicomponent fault-tolerant systems.IEEE Transactions on Reliability37(2)2.CrossRefGoogle Scholar
Gross,D. andMiller,D. (1984)The randomization technique as a modeling tool and solution procedure for transient Markov processes.Operations Research32(2)926–944.CrossRefGoogle Scholar
Haverkort,B. R. (2006) Can we quantitatively assess security? In: Workshop on Emperical Evaluation of Dependability and Security; Supplement Proceedings DSN 2006 (online) 125–128.Google Scholar
Haverkort,B. R. andNiemegeers,I. G. (1996)Performability modelling tools and techniques.Performance Evaluation2517–40.CrossRefGoogle Scholar
Haverkort,B. R.,Trivedi,K. S.,Rubino,G. andMarie,R. (eds.) (2001)Performability Modelling: Techniques and Tools,John Wiley and Sons.Google Scholar
Hermanns,H. (2002)Interactive Markov Chains: The Quest for Quantitative Quality.Springer-Verlag Lecture Notes in Computer Science2428.Google Scholar
Hermanns,H. andKatoen,J.-P. (2009)The how and why of interactive Markov chains. In: 8th International Symposium on Formal Methods for Components and Objects (FMCO).Springer-Verlag Lecture Notes in Computer Science6286311–337.Google Scholar
Hermanns,H.,Kwiatkowska,M. Z.,Norman,G.,Parker,D. andSiegle,M. (2003)On the use of MTBDDs for performability analysis and verification of stochastic systems.Journal of Logic and Algebraic Programming56(1–2)23–67.CrossRefGoogle Scholar
Howard,R. A. (1971a)Dynamic Probabilistic Systems; Volume I: Markov models,John Wiley and Sons.Google Scholar
Howard,R. A. (1971b)Dynamic Probabilistic Systems; Volume II: Semi-Markov and decision processes,John Wiley and Sons.Google Scholar
Jensen,A. (1953)Markov chains as an aid in the study of Markov processes.Skandinavisk Aktuarietidsskrift3687–91.Google Scholar
Jonsson,B. andLarsen,K. (1991)Specification and refinement of probabilistic processes. In:6th IEEE Symposium on Logic in Computer Science (LICS),IEEE Computer Society Press266–277.Google Scholar
Katoen,J.-P.,Klink,D.,Leucker,M. andWolf,V. (2007)Three-valued abstraction for continuous-time Markov chains. In:Damm,W. andHermanns,H. (eds.) Computer Aided Verification 19th International Conference, CAV 2007.Springer-Verlag Lecture Notes in Computer Science4590311–324.CrossRefGoogle Scholar
Katoen,J.-P.,Zapreev,I. S.,Hahn,E. M.,Hermanns,H. andJansen,D. N. (2011)The ins and outs of the probabilistic model checker MRMC.Performance Evaluation2(68)90–104.CrossRefGoogle Scholar
Kattenbelt,M.,Kwiatkowska,M.,Norman,G. andParker,D. (2009)Abstraction refinement for probabilistic software. In:Jones,N. andMuller-Olm,M. (eds.)Verification, Model Checking, and Abstract Interpretation (VMCAI).Springer-Verlag Lecture Notes in Computer Science5403182–197.CrossRefGoogle Scholar
Kleinrock,L. (1975)Queueing Systems; Volume 1: Theory,John Wiley and Sons.Google Scholar
Kleinrock,L. (1976)Queueing Systems; Volume 2: Computer Applications,John Wiley and Sons.Google Scholar
Kwiatkowska,M.,Norman,G. andParker,D. (2009)PRISM: Probabilistic model checking for performance and reliability analysis.ACM SIGMETRICS Performance Evaluation Review36(4)40–45.CrossRefGoogle Scholar
Larsen,K. andSkou,A. (1991)Bisimulation through probabilistic testing.Information and Computation94(1)1–28.CrossRefGoogle Scholar
Larsen,K. G. andRasmussen,J. I. (2008)Optimal reachability for multi-priced timed automata.Theoretical Computer Science390(2–3)197–213.CrossRefGoogle Scholar
Meyer,J. F. (1976)Computation-based reliability analysis.IEEE Transactions on Computers25(6)578–584.CrossRefGoogle Scholar
Meyer,J. F. (1980)On evaluating the performability of degradable computing systems.IEEE Transactions on Computers29(8)720–731.CrossRefGoogle Scholar
Meyer,J. F. (1982)Closed-form solutions of performability.IEEE Transactions on Computers31(7)648–657.CrossRefGoogle Scholar
Meyer,J. F. (1992)Performability: A retrospective and some pointers to the future.Performance Evaluation14(3)139–156.CrossRefGoogle Scholar
Meyer,J. F. (1995)Performability evaluation: Where it is and what lies ahead. In:Proceedings of the 1st International Performance and Dependability Symposium,IEEE Computer Society Press334–343.Google Scholar
Meyer,J. F. andSanders,W. H. (2001)Specification and construction of performability models. In:Performability Modelling,John Wiley and Sons.Google Scholar
Miller,B. L. (1968)Finite state continuous time Markov decision processes with a finite planning horizon.SIAM Journal on Control6(2)266–280.CrossRefGoogle Scholar
Milner,R. (1971)An algebraic definition of simulation between programs. In:Proceedings of the 2nd International Joint Conference on Artificial Intelligence,William Kaufmann481–489.Google Scholar
Milner,R. (1980)A Calculus for Communicating Processes.Springer-Verlag Lecture Notes in Computer Science92.CrossRefGoogle Scholar
Molloy,M. (1982)Performance analysis using stochastic Petri nets.IEEE Transactions on Computers31(9)913–917.CrossRefGoogle Scholar
Movaghar,A. andMeyer,J. F. (1984)Performability modelling with stochastic activity networks. In:IEEE Real-Time Systems Symposium,IEEE Computer Society Press215–224.Google Scholar
Neuhäußer,M. R. andZhang,L. (2010)Time-bounded reachability probabilities in continuous-time Markov decision processes. In:Quantitative Evaluation of Systems (QEST),IEEE Computer Society Press209–218.Google Scholar
Pattipati,K.,Li,Y. andBlom,H. (1993)A unified framework for the performability evaluation of fault-tolerant computer systems.IEEE Transactions on Computers42(3)312–326.CrossRefGoogle Scholar
Qureshi,M. A. andSanders,W. H. (1994a)Reward model solution methods with impulse and rate rewards: An algorithm and numerical results.Performance Evaluation20413–436.CrossRefGoogle Scholar
Qureshi,M. A. andSanders,W. H. (1994b)Reward model solution methods with impulse and rate rewards: an algorithm and numerical results.Performance Evaluation20(4)413–436.CrossRefGoogle Scholar
Rabe,M. andSchewe,S. (2011)Finite optimal control for time-bounded reachability in continuous-time Markov games and CTMDPs.Acta Informatica48(5–6)291–315.CrossRefGoogle Scholar
Reibman,A. andTrivedi,K. S. (1988)Numerical transient analysis of Markov models.Computers and Operations Research15(1)19–36.CrossRefGoogle Scholar
Reibman,A. andTrivedi,K. S. (1989)Transient analysis of cumulative measures of Markov model behavior.Stochastic Models5(4)683–710.CrossRefGoogle Scholar
Sanders,W. andMeyer,J. F. (1987)Performability evaluation of distributed systems using stochastic activity networks. In:Proceedings of the 2nd International Workshop on Petri Nets and Performance Models,IEEE Computer Society Press111–120.Google Scholar
Sanders,W. andMeyer,J. F. (1991)Reduced-base model construction for stochastic activity networks.IEEE Journal on Selected Areas in Communications9(1)25–36.CrossRefGoogle Scholar
Sanders,W. H. (2010)Quantitative evaluation of security metrics. In:Quantitative Evaluation of Systems (QEST),IEEE Computer Society Press 306.Google Scholar
Segala,R. andLynch,N. (1995)Probabilistic simulations for probabilistic processes.Nordic Journal of Computing2(2)250–273.Google Scholar
Sericola,B. (2000)Occupation times in Markov processes.Communications in Statistics – Stochastic Models16(5)479–510.Google Scholar
Smith,R.,Trivedi,K. S. andRamesh,A. (1988)Performability analysis: measures, an algorithm and a case study.IEEE Transactions on Computers37(4)406–417.CrossRefGoogle Scholar
Souza e Silva,E. andGail,H. (1992)Performability analysis of computer systems: from model specification to solution.Performance Evaluation1157–196.CrossRefGoogle Scholar
Tijms,H. andVeldman,R. (2000)A fast algorithm for the transient reward distribution in continuous-time Markov chains.Operation Research Letters26155–158.CrossRefGoogle Scholar
van Dijk,N. M.,Haverkort,B. R. andNiemegeers,I. G. (1992)Guest editorial: Performability modelling of computer and communication systems.Performance Evaluation14135–138.CrossRefGoogle Scholar
Wachter,B.,Zhang,L. andHermanns,H. (2007)Probabilistic model checking modulo theories. In:Quantitative Evaluation of Systems (QEST),IEEE Computer Society Press.Google Scholar
Zhang,L. andNeuhäußer,M. (2010)Model checking interactive Markov chains. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS).Springer-Verlag Lecture Notes in Computer Science601553–68.CrossRefGoogle Scholar