Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Modeling and Analysis of Timed Systems

FORMATS 2010: Formal Modeling and Analysis of Timed Systems pp 25–45Cite as

A Framework for Verification of Software with Time and Probabilities

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6246))

Abstract

Quantitative verification techniques are able to establish system properties such as “the probability of an airbag failing to deploy on demand” or “the expected time for a network protocol to successfully send a message packet”. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behaviour. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a quantitative abstraction refinement approach, which can be used to automatically construct and analyse abstractions of probabilistic, real-time programs. As a concrete example of the potential applicability of our framework, we discuss the challenges involved in applying it to the quantitative verification of SystemC, an increasingly popular system-level modelling language.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. Journal on Software Tools for Technology Transfer 1, 134–152 (1997)

    Article  MATH  Google Scholar 

  2. Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Katoen, J.-P., Hahn, E., Hermanns, H., Jansen, D., Zapreev, I.: The ins and outs of the probabilistic model checker MRMC. In: Proc. QEST’09, IEEE Press, Los Alamitos (2009)

    Google Scholar 

  4. Uppaal-PRO, http://www.cs.aau.dk/~arild/uppaal-probabilistic/

  5. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 212–227. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Hartmanns, A., Hermanns, H.: A Modest approach to checking probabilistic timed automata. In: Proc. QEST’09, pp. 187–196 (2009)

    Google Scholar 

  7. Berendsen, J., Jansen, D., Vaandrager, F.: Fortuna: Model checking priced probabilistic timed automata. In: Proc. QEST’10, IEEE Press, Los Alamitos (2010)

    Google Scholar 

  8. Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 182–197. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: Proc. QEST’06, pp. 157–166. IEEE Press, Los Alamitos (2006)

    Google Scholar 

  10. Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Technical Report RR-08-06, Oxford University Computing Laboratory (2008)

    Google Scholar 

  11. Vardi, M.: Formal techniques for SystemC verification. In: Proc. DAC’07, pp. 188–192 (2007); Position Paper

    Google Scholar 

  12. Kwiatkowska, M., Norman, G., Parker, D.: A framework for verification of software with time and probabilities (extended version), http://qav.comlab.ox.ac.uk/papers/formats10extended.pdf

  13. Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, Heidelberg (1976)

    MATH  Google Scholar 

  14. Shapley, L.: Stochastic games. Proc. National Academy of Science 39, 1095–1100 (1953)

    Article  MATH  MathSciNet  Google Scholar 

  15. Condon, A.: The complexity of stochastic games. Inf. and Comp. 96, 203–224 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  16. Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, Chichester (1994)

    MATH  Google Scholar 

  17. Wachter, B., Zhang, L.: Best probabilistic transformers. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 362–379. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL’77, pp. 238–252. ACM Press, New York (1977)

    Google Scholar 

  19. Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation 111, 193–244 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  20. Tripakis, S.: The formal analysis of timed systems in practice. PhD thesis, Université Joseph Fourier (1998)

    Google Scholar 

  21. Jensen, H.: Model checking probabilistic real time systems. In: Proc. 7th Nordic Workshop on Programming Theory, pp. 247–261 (1996)

    Google Scholar 

  22. Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282, 101–150 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  23. Beauquier, D.: Probabilistic timed automata. Theoretical Computer Science 292, 65–84 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  24. Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design 29, 33–78 (2006)

    Article  MATH  Google Scholar 

  25. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Google Scholar 

  26. Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Information and Computation 104, 2–34 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  27. Lahiri, S., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 24–38. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  28. Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design 25, 105–127 (2004)

    Article  MATH  Google Scholar 

  29. Drechsler, R., Grosse, D.: Reachability analysis for formal verification of SystemC. In: Proc. DSD’02, p. 337. IEEE Press, Los Alamitos (2002)

    Google Scholar 

  30. Kroening, D., Sharygina, N.: Formal verification of SystemC by automatic hardware/software partitioning. In: Proc. MEMOCODE’05, pp. 101–110. IEEE Press, Los Alamitos (2005)

    Google Scholar 

  31. Grosse, D., Kühne, U., Drechsler, R.: HW/SW co-verification of embedded systems using bounded model checking. In: Proc. 16th ACM Great Lakes Symp. VLSI, pp. 43–48. ACM Press, New York (2006)

    Google Scholar 

  32. Karlsson, D., Eles, P., Peng, Z.: Formal verification of SystemC designs using a Petri-net based representation. In: Proc. DATE’06, EDAA, pp. 1228–1233 (2006)

    Google Scholar 

  33. Traulsen, C., Cornet, J., Moy, M., Maraninchi, F.: A SystemC/TLM semantics in Promela and its possible applications. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 204–222. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  34. Herber, P., Fellmuth, J., Glesner, S.: Model checking SystemC designs using timed automata. In: Proc. CODES+ISSS’08, pp. 131–136 (2008)

    Google Scholar 

  35. Blanc, N., Kroening, D., Sharygina, N.: Scoot: A tool for the analysis of SystemC models. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 467–470. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  36. Moy, M., Maraninchi, F., Maillet-Contoz, L.: Pinapa: An extraction tool for SystemC descriptions of Systems-on-a-Chip. In: Proc. EMSOFT’05, pp. 317–324 (2005)

    Google Scholar 

  37. IEEE Standards Association: IEEE standard 1666: SystemC language reference manual (2005), http://www.systemc.org/

  38. Daws, C., Kwiatkowska, M., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. Int. Journal on Software Tools for Technology Transfer 5, 221–236 (2004)

    Article  Google Scholar 

  39. Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. and Comp. 205, 1027–1077 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  40. Berendsen, J., Jansen, D., Katoen, J.P.: Probably on time and within budget on reachability in priced probabilistic timed automata. In: Proc. QEST’06, pp. 311–322. IEEE Press, Los Alamitos (2006)

    Google Scholar 

  41. D’Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 57–76. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  42. Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162–175. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  43. de Alfaro, L., Roy, P.: Magnifying-lens abstraction for Markov decision processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 325–338. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  44. Chadha, R., Viswanathan, M.: A counterexample guided abstraction-refinement framework for Markov decision processes. ACM Transactions on Computational Logic (to appear, 2010)

    Google Scholar 

  45. Kemper, S., Platzer, A.: SAT-based abstraction refinement for real-time systems. In: STACS 1985. ENTCS, vol. 182, pp. 107–122 (2006)

    Google Scholar 

  46. Sorea, M.: Lazy approximation for dense real-time systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 363–378. Springer, Heidelberg (2004)

    Google Scholar 

  47. Dierks, H., Kupferschmid, S., Larsen, K.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114–129. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  48. Zbrzezny, A., Półrola: SAT-based reachability checking for timed automata with discrete data. Fundamenta Informaticae 79, 579–593 (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory, Parks Road, Oxford, OX1 3QD, UK

    Marta Kwiatkowska & David Parker

  2. Department of Computing Science, University of Glasgow, Glasgow, G12 8RZ, UK

    Gethin Norman

Authors
  1. Marta Kwiatkowska
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gethin Norman
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Parker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Science and Technology, IST Austria, Am Campus 1, 3400, Klosterneuburg, Austria

    Krishnendu Chatterjee

  2. Institute of Science and Technology, IST Austria, V, 3400, Klosterneuburg, Austria

    Thomas A. Henzinger

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kwiatkowska, M., Norman, G., Parker, D. (2010). A Framework for Verification of Software with Time and Probabilities. In: Chatterjee, K., Henzinger, T.A. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2010. Lecture Notes in Computer Science, vol 6246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15297-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15297-9_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15296-2

  • Online ISBN: 978-3-642-15297-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation