Skip to main content
SpringerLink
Log in
Book cover

Working Conference on Verified Software: Theories, Tools, and Experiments

VSTTE 2014: Verified Software: Theories, Tools and Experiments pp 235–251Cite as

Parameterized Model-Checking of Timed Systems with Conjunctive Guards

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8471))

Abstract

In this work we extend the Emerson and Kahlon’s cutoff theorems for process skeletons with conjunctive guards to Parameterized Networks of Timed Automata, i.e. systems obtained by an apriori unknown number of Timed Automata instantiated from a finite set \(U_1, \dots , U_n\) of Timed Automata templates. In this way we aim at giving a tool to universally verify software systems where an unknown number of software components (i.e. processes) interact with continuous time temporal constraints. It is often the case, indeed, that distributed algorithms show an heterogeneous nature, combining dynamic aspects with real-time aspects. In the paper we will also show how to model check a protocol that uses special variables storing identifiers of the participating processes (i.e. PIDs) in Timed Automata with conjunctive guards. This is non-trivial, since solutions to the parameterized verification problem often relies on the processes to be symmetric, i.e. indistinguishable. On the other side, many popular distributed algorithms make use of PIDs and thus cannot directly apply those solutions.

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 EPUB and 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

Notes

  1. 1.

    http://www.uppaal.com/index.php?sida=203&rubrik=92 URL visited on April’14.

  2. 2.

    The experiments were run on an Intel Core2 Duo CPU T5870 @ 2.0 Ghz with 4GB RAM, OS Linux 3.13-1-amd64.

References

  1. Abdulla, P.A., Jonsson, B.: Verifying networks of timed processes (extended abstract). In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 298–312. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  2. Abdulla, P.A., Deneux, J., Mahata, P.: Multi-clock timed networks. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science, pp. 345–354 (2004)

    Google Scholar 

  3. Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theoret. Comput. Sci. 290(1), 241–264 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  4. Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of the Fifth Symposium on Logic in Computer Science, pp. 414–425 (1990)

    Google Scholar 

  5. Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 262–281. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  6. Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22, 307–309 (1986)

    Article  MathSciNet  Google Scholar 

  7. Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 109–124. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  8. Ball, T., Levin, V., Rajamani, S.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68–76 (2011)

    Article  Google Scholar 

  9. Ben-David, S., Eisner, C., Geist, D., Wolfsthal, Y.: Model checking at IBM. Formal Methods Sys. Des. 22(2), 101–108 (2003)

    Article  MATH  Google Scholar 

  10. Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. Technical report 316, UNU-IIST (2004)

    Google Scholar 

  11. Bouajjani, A., Habermehl, P., Vojnar, T.: Verification of parametric concurrent systems with prioritised FIFO resource management. Formal Methods Syst. Des. 32, 129–172 (2008)

    Article  MATH  Google Scholar 

  12. Bouyer, P.: Model-checking timed temporal logics. Electron. Notes Theor. Comput. Sci. 231, 323–341 (2009)

    Article  MathSciNet  Google Scholar 

  13. Carioni, A., Ghilardi, S., Ranise, S.: MCMT in the land of parameterized timed automata. In: Proceedings of VERIFY@IJCAR 2010, pp. 1–16 (2010)

    Google Scholar 

  14. Clarke, E., Grumberg, O., Browne, M.: Reasoning about networks with many identical finite-state processes. In: Proceedings of the 5th Annual ACM Symposium on Principles of Distributed Computing, pp. 240–248 (1986)

    Google Scholar 

  15. Emerson, A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE-17. LNCS, vol. 1831, pp. 236–254. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Emerson, A., Namjoshi, K.: Automatic verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 87–98. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  17. Emerson, E., Namjoshi, K.: On model checking for non-deterministic infinite-state systems. In: Proceedings of 13th IEEE Symposium on Logic in Computer Science, pp. 70–80 (1998)

    Google Scholar 

  18. Emerson, E.A., Namjoshi, K.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  19. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  20. Godefroid, P.: Software model checking: The Verisoft approach. Formal Methods Syst. Des. 26(2), 77–101 (2005)

    Article  Google Scholar 

  21. Gothel, T., Glesner, S.: Towards the semi-automatic verification of parameterized real-time systems using network invariants. In: 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM), pp. 310–314 (2010)

    Google Scholar 

  22. Hanna, Y., Samuelson, D., Basu, S., Rajan, H.: Automating Cut-off for Multi-parameterized systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 338–354. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  23. Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FORTE/FMOODS 2012. LNCS, vol. 7273, pp. 18–34. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  24. Kurshan, R., McMillan, K.: A structural induction theorem for processes. In: ACM Symposium on Principles of Distributed Computing, pp. 239–247 (1989)

    Google Scholar 

  25. Mansouri-Samani, M., Mehlitz, P., Pasareanu, C., Penix, J., Brat, G., Markosian, L., O’Malley, O., Pressburger, T., Visser, W.: Program model checking-a practitioners guide. Technical report NASA/TM-2008-214577, NASA (2008)

    Google Scholar 

  26. Pagliarecci, F., Spalazzi, L., Spegni, F.: Model checking grid security. Future Gener. Comput. Syst. 29(3), 811–827 (2013)

    Article  Google Scholar 

  27. RTCA. Software Considerations in Airborne Systems and Equipment Certification. Technical report DO-178C, RTCA Inc. (2011)

    Google Scholar 

  28. Spalazzi, L., Spegni, F.: Parameterized model-checking for timed systems with conjunctive guards (extended version) (2014). arxiv:1407.7305[cs.Lo]

    Google Scholar 

  29. Yang, Q., Li, M.: A cut-off approach for bounded verification of parameterized systems. In: Proceedings of the International Conference on Software Engineering, pp. 345–354. ACM (2010)

    Google Scholar 

  30. Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comp. Lang. Syst. Struct. 30(3–4), 139–169 (2004)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DII - Università Politecnica Delle Marche, Ancona, Italy

    Luca Spalazzi & Francesco Spegni

Authors
  1. Luca Spalazzi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francesco Spegni
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Francesco Spegni .

Editor information

Editors and Affiliations

  1. NASA Ames Research Center, Mountain View, USA

    Dimitra Giannakopoulou

  2. University of Oxford, Oxford, United Kingdom

    Daniel Kroening

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Spalazzi, L., Spegni, F. (2014). Parameterized Model-Checking of Timed Systems with Conjunctive Guards. In: Giannakopoulou, D., Kroening, D. (eds) Verified Software: Theories, Tools and Experiments. VSTTE 2014. Lecture Notes in Computer Science(), vol 8471. Springer, Cham. https://doi.org/10.1007/978-3-319-12154-3_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-12154-3_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-12153-6

  • Online ISBN: 978-3-319-12154-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation