Quantitative verification: models, techniques and tools

ABSTRACT

Automated verification is a technique for establishing if certain properties, usually expressed in temporal logic, hold for a system model. The model can be defined using a high-level formalism or extracted directly from software using methods such as abstract interpretation. The verification proceeds through exhaustive exploration of the state-transition graph of the model and is therefore more powerful than testing. Quantitative verification is an analogous technique for establishing quantitative properties of a system model, such as the probability of battery power dropping below minimum, the expected time for message delivery and the expected number of messages lost before protocol termination. Models analysed through this method are typically variants of Markov chains, annotated with costs and rewards that describe resources and their usage during execution. Properties are expressed in temporal logic extended with probabilistic and reward operators. Quantitative verification involves a combination of a traversal of the state-transition graph of the model and numerical computation.

This paper gives a brief overview of current research in quantitative verification, concentrating on the potential of the method and outlining future challenges. The modelling approach is described and the usefulness of the methodology illustrated with an example of a real-world protocol standard - Bluetooth device discovery - that has been analysed using the PRISM model checker (www.prismmodelchecker.org).

REFERENCES

• 1: H. Aljazzar and S. Leue. Extended directed search for probabilistic timed reachability. In FORMATS'06, volume 4202 of LNCS, pages 33--51. Springer, 2006.
• 2: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 3: Adnan Aziz , Kumud Sanwal , Vigyan Singhal , Robert K. Brayton, Verifying Continuous Time Markov Chains, Proceedings of the 8th International Conference on Computer Aided Verification, p.269-276, August 03, 1996
• 4: Christel Baier , Edmund M. Clarke , Vassili Hartonas-Garmhausen , Marta Z. Kwiatkowska , Mark Ryan, Symbolic Model Checking for Probabilistic Processes, Proceedings of the 24th International Colloquium on Automata, Languages and Programming, p.430-440, July 07-11, 1997
• 5: Christel Baier , Joost-Pieter Katoen , Holger Hermanns, Approximate Symbolic Model Checking of Continuous-Time Markov Chains, Proceedings of the 10th International Conference on Concurrency Theory, p.146-161, August 24-27, 1999
• 6: Christel Baier , Marta Kwiatkowska, Model checking for a probabilistic branching time logic with fairness, Distributed Computing, v.11 n.3, p.125-155, August 1998 [doi>10.1007/s004460050046]
• 7: Dimitri P. Bertsekas, Dynamic Programming and Optimal Control, Two Volume Set, Athena Scientific, 1995
• 8: Andrea Bianco , Luca de Alfaro, Model Checking of Probabalistic and Nondeterministic Systems, Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science, p.499-513, December 18-20, 1995
• 9: S. Cattani, R. Segala, M. Kwiatkowska, and G. Norman. Stochastic transition systems for continuous state spaces and non-determinism. In Proc. FOSSACS'05, volume 3441 of LNCS, pages 125--139. Springer Verlag, 2005.
• 10: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 11: C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite state probabilistic programs. In Proc. FOCS'88, pages 338--345. IEEE CS Press, 1988.
• 12: Costas Courcoubetis , Mihalis Yannakakis, The complexity of probabilistic verification, Journal of the ACM (JACM), v.42 n.4, p.857-907, July 1995 [doi>10.1145/210332.210339]
• 13: Marie Duflot , Marta Kwiatkowska , Gethin Norman , David Parker, A formal analysis of bluetooth device discovery, International Journal on Software Tools for Technology Transfer (STTT), v.8 n.6, p.621-632, October 2006 [doi>10.1007/s10009-006-0014-x]
• 14: Stefan Edelkamp , Stefan Leue , Alberto Lluch-Lafuente, Directed explicit-state model checking in the validation of communication protocols, International Journal on Software Tools for Technology Transfer (STTT), v.5 n.2, p.247-267, March 2004 [doi>10.1007/s10009-002-0104-3]
• 15: H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512--535, 1994.
• 16: J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn. Probabilistic model checking of complex biological pathways. In C. Priami, editor, Proc. Computational Methods in Systems Biology (CMSB'06), volume 4210 of Lecture Notes in Bioinformatics, pages 32--47. Springer Verlag, 2006.
• 17: T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet. Approximate probabilistic model checking. In Proc. VMCAI'04, volume 2937 of LNCS. Springer, 2004.
• 18: A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In Proc. TACAS'06, volume 3920 of LNCS, pages 441--444. Springer, 2006.
• 19: J. Kemeny, J. Snell, and A. Knapp. Denumerable Markov Chains. D. Van Nostrand Company, 1966.
• 20: Marta Kwiatkowska, Model checking for probability and time: from theory to practice, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.351, June 22-25, 2003
• 21: Marta Kwiatkowska , Gethin Norman , David Parker, Probabilistic symbolic model checking with PRISM: a hybrid approach, International Journal on Software Tools for Technology Transfer (STTT), v.6 n.2, p.128-142, August 2004 [doi>10.1007/s10009-004-0140-2]
• 22: Marta Kwiatkowska , Gethin Norman , David Parker, Probabilistic model checking in practice: case studies with PRISM, ACM SIGMETRICS Performance Evaluation Review, v.32 n.4, p.16-21, March 2005 [doi>10.1145/1059816.1059820]
• 23: M. Kwiatkowska, G. Norman, and D. Parker. Quantitative analysis with the probabilistic model checker PRISM. Electronic Notes in Theoretical Computer Science, 153(2):5--31, 2005.
• 24: M. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking. In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of LNCS (Tutorial Volume), pages 220--270. Springer, 2007.
• 25: Marta Kwiatkowska , Gethin Norman , David Parker , Jeremy Sproston, Performance analysis of probabilistic timed automata using digital clocks, Formal Methods in System Design, v.29 n.1, p.33-78, July 2006 [doi>10.1007/s10703-006-0005-2]
• 26: M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston. Verification of real-time probabilistic systems. In S. Mertz and N. Navet, editors, Modelling and Verification of Real-Time Systems, 2007. To appear.
• 27: Marta Z. Kwiatkowska , Gethin Norman , Roberto Segala , Jeremy Sproston, Verifying Quantitative Properties of Continuous Probabilistic Timed Automata, Proceedings of the 11th International Conference on Concurrency Theory, p.123-137, August 22-25, 2000
• 28: Marta Kwiatkowska , Gethin Norman , Roberto Segala , Jeremy Sproston, Automatic verification of real-time systems with discrete probability distributions, Theoretical Computer Science, v.282 n.1, p.101-150, June 7, 2002 [doi>10.1016/S0304-3975(01)00046-9]
• 29: Marta Kwiatkowska , Gethin Norman , Jeremy Sproston , Fuzhi Wang, Symbolic model checking for probabilistic timed automata, Information and Computation, v.205 n.7, p.1027-1077, July, 2007 [doi>10.1016/j.ic.2007.01.004]
• 30: PRISM web site: www.prismmodelchecker.org.
• 31: Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, John Wiley & Sons, Inc., New York, NY, 1994
• 32: 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. AMS, 2004.
• 33: K. Sen, M. Viswanathan, and G. Agha. On statistical model checking of stochastic systems. In Proc. CAV'05, volume 3576 of LNCS, pages 266--280. Springer, 2005.
• 34: W. J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton, 1994.
• 35: M. Vardi. Automatic verification of probabilistic concurrent finite state programs. In Proc. 26th Annual Symposium on Foundations of Computer Science (FOCS'85), pages 327--338. IEEE CS Press, 1985.
• 36: Håkan L. S. Younes , Marta Kwiatkowska , Gethin Norman , David Parker, Numerical vs. statistical probabilistic model checking, International Journal on Software Tools for Technology Transfer (STTT), v.8 n.3, p.216-228, June 2006 [doi>10.1007/s10009-005-0187-8]
• 37: Håkan L. S. Younes , Reid G. Simmons, Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling, Proceedings of the 14th International Conference on Computer Aided Verification, p.223-235, July 27-31, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Statistical methods; Model checking

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs; Mechanical verification

General Terms:
Performance, Reliability, Theory, Verification

Keywords:
Markov models, probabilistic model checking, probabilistic temporal logics, quantitative model checking