Hostname: page-component-8448b6f56d-42gr6 Total loading time: 0 Render date: 2024-04-19T03:38:54.149Z Has data issue: false hasContentIssue false
  • English
  • Français

Model checking for performability

Published online by Cambridge University Press:  08 July 2013

C. BAIER ,
E. M. HAHN ,
B. R. HAVERKORT ,
H. HERMANNS  and
J.-P. KATOEN
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
Get access Rights & Permissions [Opens in a new window]

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
Information
Mathematical Structures in Computer Science , Volume 23 , Special Issue 4: Lightweight and Practical Formal Methods in the Design and Analysis of Safety-Critical Systems , August 2013 , pp. 751 - 795
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.)

References

Abate, A., Katoen, J.-P. and Mereacre, A. (2011) Quantitative automata model checking of autonomous stochastic hybrid systems. In: Hybrid Systems: Computation and Control (HSCC), ACM 83–92.Google Scholar
Abate, A., Prandini, M., Lygeros, J. and Sastry, S. (2008) Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44 (11)2724–2734.CrossRefGoogle Scholar
Ajmone Marsan, M., Conte, G. and Balbo, G. (1984) A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Transactions on Computer Systems 2 93–122.CrossRefGoogle Scholar
Aldini, A. and Bernardo, M. (2007) Mixing logics and rewards for the component-oriented specification of performance measures. Theoretical Computer Science 382 3–23.CrossRefGoogle Scholar
Arnold, T. (1973) The concept of coverage and its effect on the reliability model of a repairable system. IEEE Transactions on Computers 22 251–254.CrossRefGoogle Scholar
Avizienis, A., Laprie, J.-C., Randell, B. and Landwehr, C. E. (2004) Basic concepts and taxonomy of dependable and secure computing. IEEE Transactions on Dependable and Secure Computing 1 (1)11–33.CrossRefGoogle Scholar
Aziz, A., Sanwal, K., Singhal, V. and Brayton, R. K. (2000) Model-checking continuous-time Markov chains. ACM Transactions on Computational Logic 1 (1)162–170.CrossRefGoogle Scholar
Baier, C., Cloth, L., Haverkort, B. R., Hermanns, H. and Katoen, J.-P. (2010a) Performability assessment by model checking of Markov reward models. Formal Methods in System Design 36 (1)1–36.CrossRefGoogle Scholar
Baier, C., Haverkort, B. R., Hermanns, H. and Katoen, J. (2000) On the logical characterisation of performability properties. In: International Colloquium on Automata, Languages, and Programming (ICALP). Springer-Verlag Lecture Notes in Computer Science 1853 780–792.CrossRefGoogle Scholar
Baier, C., Haverkort, B. R., Hermanns, H. and Katoen, J.-P. (2003) Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29 524–541.CrossRefGoogle Scholar
Baier, C., Haverkort, B. R., Hermanns, H. and Katoen, J.-P. (2008) Reachability in continuous-time Markov reward decision processes. In: Flum, J., Grädel, E. and Wilke, T. (eds.) Logic and Automata, Texts in Logic and Games 2, Amsterdam University Press 53–72.Google Scholar
Baier, C., Haverkort, B. R., Hermanns, H. and Katoen, J.-P. (2010b) Performance evaluation and model checking join forces. Communications of the ACM 53 76–85.CrossRefGoogle Scholar
Baier, C. and Hermanns, H. (1997) Weak bisimulation for fully probabilistic processes. In: Computer Aided Verification (CAV). Springer-Verlag Lecture Notes in Computer Science 1254 119–130.CrossRefGoogle Scholar
Baier, C., Hermanns, H., Katoen, J.-P. and Haverkort, B. R. (2005a) Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science 345 (1)2–26.CrossRefGoogle Scholar
Baier, C. and Katoen, J.-P. (2008) Principles of Model Checking, MIT Press.Google Scholar
Baier, C., Katoen, J.-P. and Hermanns, H. (1999) Approximate symbolic model checking of continuous-time Markov chains. In: Concurrency Theory (CONCUR). Springer-Verlag Lecture Notes in Computer Science 1664 146–161.CrossRefGoogle Scholar
Baier, C., Katoen, J.-P., Hermanns, H. and Wolf, V. (2005b) Comparative branching-time semantics for Markov chains. Information and Computation 200 (2)149–214.CrossRefGoogle Scholar
Beaudry, M. (1978) Performance-related reliability measures for computing systems. IEEE Transactions on Computer Systems 27 (6)540–547.CrossRefGoogle Scholar
Berendsen, J., Jansen, D. N. and Katoen, 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 Press 311–322.Google Scholar
Bernardo, M. and Bravetti, 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 Science 2165 136–151.CrossRefGoogle Scholar
Brázdil, T., Forejt, V., Krčál, J., Křetínský, J., and Kučera, A. (2009) Continuous-time stochastic games with time-bounded reachability. In: FSTTCS. LIPIcs 4, Schloss Dagstuhl 61–72.Google Scholar
Buchholz, P., Hahn, E. M., Hermanns, H. and Zhang, L. (2011) Model checking algorithms for CTMDPs. In: CAV. Springer-Verlag Lecture Notes in Computer Science 6806 225–242.CrossRefGoogle Scholar
Caillaud, B., Delahaye, B., Larsen, K., Legay, A., Pedersen, M. and Wasowski, A. (2010) Compositional design methodology with constraint Markov chains. In: Quantitative Evaluation of Systems (QEST), IEEE Computer Society Press 123–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 Press 136–143.Google Scholar
Ciardo, G., Jones, R. L. III, Miner, A. S. and Siminiceanu, R. (2003) Logical and stochastic modeling with SMART. In: Computer Performance Evaluation/TOOLS. Springer-Verlag Lecture Notes in Computer Science 2794 78–97.CrossRefGoogle Scholar
Ciardo, G., Miner, A. S., Wan, M. and Yu, A. J. (2007) Approximating stationary measures of structured continuous-time Markov models using matrix diagrams. ACM SIGMETRICS Performance Evaluation Review 35 (3)16–18.CrossRefGoogle Scholar
Clarke, E. M., Emerson, E. A. and Sistla, A. P. (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8 244–263.CrossRefGoogle Scholar
Cloth, L. and Haverkort, B. R. (2005) Model checking for survivability! In: Quantitative Evaluation of Systems (QEST), IEEE Computer Society 145–154.Google Scholar
Cloth, L., Jongerden, M. R. and Haverkort, 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 Society 780–789.Google Scholar
Desharnais, J. and Panangaden, P. (2003) Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. Journal of Logic and Algebraic Programming 56 (1–2)99–115.CrossRefGoogle Scholar
Donatiello, L. and Iyer, B. (1987a) Analysis of a composite performance reliability measure for fault-tolerant systems. Journal of the ACM 34 (1)179–199.CrossRefGoogle Scholar
Donatiello, L. and Iyer, B. (1987b) Closed-form solution for system availability. IEEE Transactions on Reliability 36 (1)45–47.CrossRefGoogle Scholar
Furchtgott, D. and Meyer, J. F. (1984) A performability solution method for degradable non-repairable systems. IEEE Transactions on Computers 33 (6)550–554.CrossRefGoogle Scholar
Gay, F. A. and Ketelsen, M. L. (1979) Performance evaluation for gracefully degrading systems. In: Proceedings of the 9th Fault-Tolerant Computer Systems Systems (FTCS), IEEE Computer Society Press 51–58.Google Scholar
Geist, R. and Trivedi, K. S. (1990) Reliability estimation of fault-tolerant systems: Tools and techniques. Computer 23 (7)52–61.CrossRefGoogle Scholar
Ghemawat, S., Gobioff, H. and Leung, S.-T. (2003) The Google file system. In: ACM Symposium on Operating Systems Principles (SOSP), ACM 29–43.CrossRefGoogle Scholar
Goyal, A., Lavenberg, S. and Trivedi, K. S. (1987) The system availability estimator. Annals of Operations Research 8 285–306.CrossRefGoogle Scholar
Goyal, A. and Tantawi, A. (1988) A measure of guaranteed availability and its numerical evaluation. IEEE Transactions on Computers 37 (1)25–32.CrossRefGoogle Scholar
Goyal, A. and Tantawi, A. N. (1987) Evaluation of performability for degradable computer systems. IEEE Transactions on Computers 36 (6)7.Google Scholar
Grassi, V., Donatiello, L. and Iazeolla, G. (1988) Performability evaluation of multicomponent fault-tolerant systems. IEEE Transactions on Reliability 37 (2)2.CrossRefGoogle Scholar
Gross, D. and Miller, D. (1984) The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research 32 (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. and Niemegeers, I. G. (1996) Performability modelling tools and techniques. Performance Evaluation 25 17–40.CrossRefGoogle Scholar
Haverkort, B. R., Trivedi, K. S., Rubino, G. and Marie, 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 Science 2428.Google Scholar
Hermanns, H. and Katoen, 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 Science 6286 311–337.Google Scholar
Hermanns, H., Kwiatkowska, M. Z., Norman, G., Parker, D. and Siegle, M. (2003) On the use of MTBDDs for performability analysis and verification of stochastic systems. Journal of Logic and Algebraic Programming 56 (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 Aktuarietidsskrift 36 87–91.Google Scholar
Jonsson, B. and Larsen, K. (1991) Specification and refinement of probabilistic processes. In: 6th IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press 266–277.Google Scholar
Katoen, J.-P., Klink, D., Leucker, M. and Wolf, V. (2007) Three-valued abstraction for continuous-time Markov chains. In: Damm, W. and Hermanns, H. (eds.) Computer Aided Verification 19th International Conference, CAV 2007. Springer-Verlag Lecture Notes in Computer Science 4590 311–324.CrossRefGoogle Scholar
Katoen, J.-P., Zapreev, I. S., Hahn, E. M., Hermanns, H. and Jansen, D. N. (2011) The ins and outs of the probabilistic model checker MRMC. Performance Evaluation 2 (68)90–104.CrossRefGoogle Scholar
Kattenbelt, M., Kwiatkowska, M., Norman, G. and Parker, D. (2009) Abstraction refinement for probabilistic software. In: Jones, N. and Muller-Olm, M. (eds.) Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer-Verlag Lecture Notes in Computer Science 5403 182–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. and Parker, D. (2009) PRISM: Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review 36 (4)40–45.CrossRefGoogle Scholar
Larsen, K. and Skou, A. (1991) Bisimulation through probabilistic testing. Information and Computation 94 (1)1–28.CrossRefGoogle Scholar
Larsen, K. G. and Rasmussen, J. I. (2008) Optimal reachability for multi-priced timed automata. Theoretical Computer Science 390 (2–3)197–213.CrossRefGoogle Scholar
Meyer, J. F. (1976) Computation-based reliability analysis. IEEE Transactions on Computers 25 (6)578–584.CrossRefGoogle Scholar
Meyer, J. F. (1980) On evaluating the performability of degradable computing systems. IEEE Transactions on Computers 29 (8)720–731.CrossRefGoogle Scholar
Meyer, J. F. (1982) Closed-form solutions of performability. IEEE Transactions on Computers 31 (7)648–657.CrossRefGoogle Scholar
Meyer, J. F. (1992) Performability: A retrospective and some pointers to the future. Performance Evaluation 14 (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 Press 334–343.Google Scholar
Meyer, J. F. and Sanders, 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 Control 6 (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 Kaufmann 481–489.Google Scholar
Milner, R. (1980) A Calculus for Communicating Processes. Springer-Verlag Lecture Notes in Computer Science 92.CrossRefGoogle Scholar
Molloy, M. (1982) Performance analysis using stochastic Petri nets. IEEE Transactions on Computers 31 (9)913–917.CrossRefGoogle Scholar
Movaghar, A. and Meyer, J. F. (1984) Performability modelling with stochastic activity networks. In: IEEE Real-Time Systems Symposium, IEEE Computer Society Press 215–224.Google Scholar
Neuhäußer, M. R. and Zhang, L. (2010) Time-bounded reachability probabilities in continuous-time Markov decision processes. In: Quantitative Evaluation of Systems (QEST), IEEE Computer Society Press 209–218.Google Scholar
Pattipati, K., Li, Y. and Blom, H. (1993) A unified framework for the performability evaluation of fault-tolerant computer systems. IEEE Transactions on Computers 42 (3)312–326.CrossRefGoogle Scholar
Qureshi, M. A. and Sanders, W. H. (1994a) Reward model solution methods with impulse and rate rewards: An algorithm and numerical results. Performance Evaluation 20 413–436.CrossRefGoogle Scholar
Qureshi, M. A. and Sanders, W. H. (1994b) Reward model solution methods with impulse and rate rewards: an algorithm and numerical results. Performance Evaluation 20 (4)413–436.CrossRefGoogle Scholar
Rabe, M. and Schewe, S. (2011) Finite optimal control for time-bounded reachability in continuous-time Markov games and CTMDPs. Acta Informatica 48 (5–6)291–315.CrossRefGoogle Scholar
Reibman, A. and Trivedi, K. S. (1988) Numerical transient analysis of Markov models. Computers and Operations Research 15 (1)19–36.CrossRefGoogle Scholar
Reibman, A. and Trivedi, K. S. (1989) Transient analysis of cumulative measures of Markov model behavior. Stochastic Models 5 (4)683–710.CrossRefGoogle Scholar
Sanders, W. and Meyer, 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 Press 111–120.Google Scholar
Sanders, W. and Meyer, J. F. (1991) Reduced-base model construction for stochastic activity networks. IEEE Journal on Selected Areas in Communications 9 (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. and Lynch, N. (1995) Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2 (2)250–273.Google Scholar
Sericola, B. (2000) Occupation times in Markov processes. Communications in Statistics – Stochastic Models 16 (5)479–510.Google Scholar
Smith, R., Trivedi, K. S. and Ramesh, A. (1988) Performability analysis: measures, an algorithm and a case study. IEEE Transactions on Computers 37 (4)406–417.CrossRefGoogle Scholar
Souza e Silva, E. and Gail, H. (1992) Performability analysis of computer systems: from model specification to solution. Performance Evaluation 1 157–196.CrossRefGoogle Scholar
Tijms, H. and Veldman, R. (2000) A fast algorithm for the transient reward distribution in continuous-time Markov chains. Operation Research Letters 26 155–158.CrossRefGoogle Scholar
van Dijk, N. M., Haverkort, B. R. and Niemegeers, I. G. (1992) Guest editorial: Performability modelling of computer and communication systems. Performance Evaluation 14 135–138.CrossRefGoogle Scholar
Wachter, B., Zhang, L. and Hermanns, H. (2007) Probabilistic model checking modulo theories. In: Quantitative Evaluation of Systems (QEST), IEEE Computer Society Press.Google Scholar
Zhang, L. and Neuhä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 Science 6015 53–68.CrossRefGoogle Scholar