Skip to main content
SpringerLink
Log in

Statistical Model Checking for Networks of Priced Timed Automata

  • Conference paper
Formal Modeling and Analysis of Timed Systems (FORMATS 2011)

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

Abstract

This paper offers a natural stochastic semantics of Networks of Priced Timed Automata (NPTA) based on races between components. The semantics provides the basis for satisfaction of Probabilistic Weighted CTL properties (PWCTL), conservatively extending the classical satisfaction of timed automata with respect to TCTL. In particular the extension allows for hard real-time properties of timed automata expressible in TCTL to be refined by performance properties, e.g. in terms of probabilistic guarantees of time- and cost-bounded properties. A second contribution of the paper is the application of Statistical Model Checking (SMC) to efficiently estimate the correctness of non-nested PWCTL model checking problems with a desired level of confidence, based on a number of independent runs of the NPTA. In addition to applying classical SMC algorithms, we also offer an extension that allows to efficiently compare performance properties of NPTAs in a parametric setting. The third contribution is an efficient tool implementation of our result and applications to several case studies.

Work partially supported by VKR Centre of Excellence – MT-LAB and by an “Action de Recherche Collaborative” ARC (TP)I.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3–34 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) [7], pp. 49–62

    Google Scholar 

  4. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M.: Probabilistic and topological semantics for timed automata. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 179–191. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) [7], pp. 147–161

    Google Scholar 

  7. Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.): HSCC 2001. LNCS, vol. 2034. Springer, Heidelberg (2001)

    Google Scholar 

  8. Bertrand, N., Bouyer, P., Brihaye, T., Markey, N.: Quantitative model-checking of one-clock timed automata under probabilistic semantics. In: QEST, pp. 55–64. IEEE Computer Society, Los Alamitos (2008)

    Google Scholar 

  9. Bogdoll, J., Fiorti, L.-M., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 59–74. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  10. Bohnenkamp, H., D’Argenio, P.R., Hermanns, H., Katoen, J.-P.: Modest: A compositional modeling formalism for real-time and stochastic systems. Technical Report CTIT 04-46, University of Twente (2004)

    Google Scholar 

  11. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  12. Clarke, E.M., Donzé, A., Legay, A.: Statistical model checking of mixed-analog circuits with an application to a third order delta-sigma modulator. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 149–163. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  13. David, A., Larsen, K.G., Legay, A., Wang, Z., Mikucionis, M.: Time for real statistical model-checking: Statistical model-checking for real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: HSCC. ACM, New York (2010)

    Google Scholar 

  15. Fehnker, A., van Hoesel, L., Mader, A.: Modelling and verification of the lmac protocol for wireless sensor networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 253–272. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. STTT 10(3), 263–279 (2008)

    Article  MATH  Google Scholar 

  17. Gómez, R.: A compositional translation of timed automata with deadlines to uppaal timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 179–194. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  18. Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  20. Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  21. Kaczmarczyk, V., Sir, M., Bradac, Z.: Stochastic timed automata simulator. In: 4th European Computing Conference. WSEAS

    Google Scholar 

  22. Kaczmarczyk, V., Sir, M., Bradac, Z.: Stochastic timed automata simulator. In: Proceedings of the 4th European Computing Conference (2010)

    Google Scholar 

  23. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: POPL, pp. 344–352 (1989)

    Google Scholar 

  24. Maler, O., Larsen, K.G., Krogh, B.H.: On zone-based analysis of duration probabilistic automata. In: INFINITY. EPTCS, vol. 39, pp. 33–46 (2010)

    Google Scholar 

  25. Minea, M.: Partial Order Reduction for Verification of Timed Systems. PhD thesis, Carnegie Mellon (1999)

    Google Scholar 

  26. Panangaden, P.: Labelled Markov Processes. Imperial College Press (2010)

    Google Scholar 

  27. Poulsen, D., van Vliet, J.: Duration probabilistic automata. Technical report, Aalborg University (2011)

    Google Scholar 

  28. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  29. The smv model checker, http://www.kenmcmil.com/smv.html

  30. The spin tool (spin), http://spinroot.com/spin/whatispin.html

  31. Teige, T., Eggers, A., Fränzle, M.: Constraint-based analysis of concurrent probabilistic hybrid systems: An application to networked automation systems. In: Nonlinear Analysis: Hybrid Systems (2011)

    Google Scholar 

  32. The uppaal tool, http://www.uppaal.com/

  33. van Hoesel, L.F.W.: Sensors on speaking terms: schedule-based medium access control protocols for wireless sensor networks. PhD thesis, University of Twente (June 2007)

    Google Scholar 

  34. Wald, R.: Sequential Analysis. Dove Publisher (2004)

    Google Scholar 

  35. Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Carnegie Mellon (2005)

    Google Scholar 

  36. Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  37. Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  38. Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: HSCC, pp. 243–252. ACM, New York (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Aalborg University, Denmark

    Alexandre David, Kim G. Larsen, Marius Mikučionis, Danny Bøgsted Poulsen & Jonas van Vliet

  2. INRIA/IRISA Rennes, France

    Axel Legay

  3. East China Normal University, China

    Zheng Wang

Authors
  1. Alexandre David
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Marius Mikučionis
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Danny Bøgsted Poulsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Jonas van Vliet
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Zheng Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IRISA/INRIA Rennes, Campus Beaulieu, 35042, Rennes Cedex, France

    Uli Fahrenberg

  2. University of California, 94720-1770, Berkeley, CA, USA

    Stavros Tripakis

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

David, A. et al. (2011). Statistical Model Checking for Networks of Priced Timed Automata. In: Fahrenberg, U., Tripakis, S. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2011. Lecture Notes in Computer Science, vol 6919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24310-3_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24310-3_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24309-7

  • Online ISBN: 978-3-642-24310-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation