Probabilistic model checking in practice: case studies with PRISM

ABSTRACT

In this paper, we describe some practical applications of probabilistic model checking, a technique for the formal analysis of systems which exhibit stochastic behaviour. We give an overview of a selection of case studies carried out using the probabilistic model checking tool PRISM, demonstrating the wide range of application domains to which these methods are applicable. We also illustrate several benefits of using formal verification techniques to analyse probabilistic systems, including: (i) that they allow a wide range of numerical properties to be computed accurately; and (ii) that they perform a complete and exhaustive analysis enabling, for example, a study of best- and worst-case scenarios.

REFERENCES

• 1: PRISM web site. www.cs.bham.ac.uk/~dxp/prism.
• 2: C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, 29(6):524--541, 2003.
• 3: M. Duflot, L. Fribourg, T. Hérault, R. Lassaigne, F. Magniette, S. Messika, S. Peyronnet, and C. Picaronny. Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC. In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04). Elsevier Science, Electronic Notes in Theoretical Computer Science Science, 2004. To appear.
• 4: M. Duflot, M. Kwiatkowska, G. Norman, and D. Parker. A formal analysis of Bluetooth device discovery. In Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04), 2004. To appear.
• 5: Shimon Even , Oded Goldreich , Abraham Lempel, A randomized protocol for signing contracts, Communications of the ACM, v.28 n.6, p.637-647, June 1985 [doi>10.1145/3812.3818]
• 6: W. Fokkink and J. Pang. Simplifying Itai-Rodeh leader election for anonymous rings. In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04). Elsevier Science, Electronic Notes in Theoretical Computer Science Science, 2004. To appear.
• 7: J. Han and P. Jonker. A system architecture solution for unreliable nanoelectronic devices. IEEE Transactions on Nanotechnology, 1:201--208, 12002.
• 8: T. Herman, Probabilistic self-stabilization, Information Processing Letters, v.35 n.2, p.63-67, June 1990 [doi>10.1016/0020-0190(90)90107-9]
• 9: Holger Hermanns , Joost-Pieter Katoen , Joachim Meyer-Kayser , Markus Siegle, A Markov Chain Model Checker, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.347-362, March 25-April 02, 2000
• 10: B. Jeannet, P. D'Argenio, and K. Larsen. RAPTURE: A tool for verifying Markov decision processes. In I. Cerna, editor, Proc. Tools Day, affiliated to 13th Int. Conf. Concurrency Theory (CONCUR'02), Technical Report FIMU-RS-2002--05, Faculty of Informatics, Masaryk University, pages 84--98, 2002.
• 11: Marta Z. Kwiatkowska , Gethin Norman, Verifying Randomized Byzantine Agreement, Proceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems, p.194-209, November 11-14, 2002
• 12: Marta Kwiatkowska , Gethin Norman , David Parker, PRISM 2.0: A Tool for Probabilistic Model Checking, Proceedings of the The Quantitative Evaluation of Systems, First International Conference on (QEST'04), p.322-323, September 27-30, 2004 [doi>10.1109/QEST.2004.35]
• 13: M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston. Performance analysis of probabilistic timed automata using digital clocks. In K. Larsen and P. Niebert, editors, Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03), volume 2791 of LNCS, pages 105--120. Springer-Verlag, 2003.
• 14: Marta Z. Kwiatkowska , Gethin Norman , Roberto Segala, Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM, Proceedings of the 13th International Conference on Computer Aided Verification, p.194-206, July 18-22, 2001
• 15: Marta Z. Kwiatkowska , Gethin Norman , Jeremy Sproston, Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol, Proceedings of the Second Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, p.169-187, July 25-26, 2002
• 16: M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Special Issue of Formal Aspects of Computing, 14:295--318, 2003.
• 17: M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic model checking for probabilistic timed automata. In Y. Lakhnech and S. Yovine, editors, Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT), volume 3253 of LNCS, pages 293--308. Springer, 2004.
• 18: R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Automatic analysis of a non-repudiation protocol. In Proc. 2nd International Workshop on Quantitative Aspects of Programming Languages (QAPL'04), 2004.
• 19: P. Lecca and C. Priami. Cell cycle control in eukaryotes: A BioSpi model. In Proc. Workshop on Concurrent Models in Molecular Biology (BioConcur'03), Electronic Notes in Theoretical Computer Science, 2003.
• 20: A. McIver and C. Morgan. An elementary proof that Herman's ring is θ(n2). Submitted for publication.
• 21: G. Norman, D. Parker, M. Kwiatkowska, and S. Shukla. Evaluating the reliability of NAND multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2005. To appear.
• 22: G. Norman , D. Parker , M. Kwiatkowska , S. K. Shukla , R. K. Gupta, Formal analysis and validation of continuous-time Markov chain based system level power management strategies, Proceedings of the Seventh IEEE International High-Level Design Validation and Test Workshop (HLDVT'02), p.45, October 27-29, 2002
• 23: G. Norman, D. Parker, M. Kwiatkowska, S. Shukla, and R. Gupta. Using probabilistic model checking for dynamic power management. In M. Leuschel, S. Gruner, and S. L. Presti, editors, Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03), Technical Report DSSE-TR-2003-2. University of Southampton, pages 202--215, April 2003.
• 24: G. Norman and V. Shmatikov. Analysis of probabilistic contract signing. In A. Abdallah, P. Ryan, and S. Schneider, editors, Proc. BCS-FACS Formal Aspects of Security (FASec'02), volume 2629 of LNCS, pages 81--96. Springer, 2003.
• 25: G. Norman and V. Shmatikov. Analysis of probabilistic contract signing. Submitted, 2005.
• 26: Padmanabhan Pillai , Kang G. Shin, Real-time dynamic voltage scaling for low-power embedded operating systems, ACM SIGOPS Operating Systems Review, v.35 n.5, Dec. 2001
• 27: J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.), volume 23 of CRM Monograph Series. American Mathematical Society, 2004.
• 28: V. Shmatikov. Probabilistic model checking of an anonymity system. Journal of Computer Security, 12(3/4):355--377, 2004.
• 29: M. Stoelinga. Alea jacta est: Verification of probabilistic, real-time and parametric systems. PhD thesis, University of Nijmegen, 2002.
• 30: J. von Neumann. Probabilistic logics and synthesis of reliable organisms from unreliable components. In C. Shannon and J. McCarthy, editors, Automata Studies, pages 43--98. Princeton University Press, 1956.

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.1 MODELS AND PRINCIPLES
      H.1.1 Systems and Information Theory
          Subjects: General systems theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: PRISM

  G. Mathematics of Computing
  G.3 PROBABILITY AND STATISTICS
      Subjects: Probabilistic algorithms (including Monte Carlo)

General Terms:
Algorithms, Measurement, Performance