Skip to main content
SpringerLink
Log in
Book cover

NASA Formal Methods Symposium

NFM 2015: NASA Formal Methods pp 66–81Cite as

Compositional Verification of Parameterised Timed Systems

  • Conference paper
  • First Online:

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

Abstract

In this paper we address the problem of uniform verification of parameterised timed systems (PTS): “does a given safety state property hold for a system containing n identical timed components regardless of the value of n?”. Our approach is compositional and consequently it suits quite well such systems in that it presents the advantage of reusing existing local characterisations at the global level of system characterisation. Additionally, we show how a direct consequence of the modelling choices adopted in our framework leads to an elegant application of the presented method to topologies such as stars and rings.

Work partially supported by the European Projects 257414 ASCENS, STREP 318772 D-MILS, French BGLE Manycorelabs, and Artemis AIPP Arrowhead.

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. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS (1996)

    Google Scholar 

  2. Abdulla, P.A., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R.: On the Verification of Timed Ad Hoc Networks. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 256–270. Springer, Heidelberg (2011)

    Google Scholar 

  3. Abdulla, P.A., Deneux, J., Mahata, P.: Closed, open, and robust timed networks. ENTCS 138(3) (2005)

    Google Scholar 

  4. Abdulla, P.A., Jonsson, B.: On the Existence of Network Invariants for Verifying Parameterized Systems. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 180–197. Springer, Heidelberg (1999)

    Google Scholar 

  5. Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theor. Comput. Sci. 290(1) (2003)

    Google Scholar 

  6. Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A Survey of Regular Model Checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004)

    Google Scholar 

  7. Alur, R.: Timed Automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)

    Google Scholar 

  8. Alur, R., Courcoubetis, C., Dill, D.L., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: RTSS (1992)

    Google Scholar 

  9. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. (1994)

    Google Scholar 

  10. Aştefănoaei, L., Ben Rayana, S., Bensalem, S., Bozga, M., Combaz, J.: Compositional Invariant Generation for Timed Systems. In: \’{A}brahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 263–278. Springer, Heidelberg (2014)

    Google Scholar 

  11. Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting WS1S Systems to Verify Parameterized Networks. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 188–203. Springer, Heidelberg (2000)

    Google Scholar 

  12. Baukus, K., Stahl, K., Bensalem, S., Lakhnech, Y.: Networks of processes with parameterized state space. ENTCS 50(4) (2001)

    Google Scholar 

  13. Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional Verification for Component-Based Systems and Application. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64–79. Springer, Heidelberg (2008)

    Google Scholar 

  14. Bouajjani, A., Jurski, Y., Sighireanu, M.: A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 690–705. Springer, Heidelberg (2007)

    Google Scholar 

  15. Bruttomesso, R., Carioni, A., Ghilardi, S., Ranise, S.: Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 279–294. Springer, Heidelberg (2012)

    Google Scholar 

  16. Carioni, A., Ghilardi, S., Ranise, S.: Mcmt in the land of parametrized timed automata. In: VERIFY@IJCAR (2010)

    Google Scholar 

  17. Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: CADE (2000)

    Google Scholar 

  18. Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL (1995)

    Google Scholar 

  19. Emerson, E.A., Sistla, A. P.: Symmetry and model checking. Formal Methods in System Design 9(1/2) (1996)

    Google Scholar 

  20. Finkel, A.: A generalization of the procedure of karp and miller to well structured transition systems. In: ICALP (1987)

    Google Scholar 

  21. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2) (2001)

    Google Scholar 

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

    Google Scholar 

  23. Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT Model Checking of Array-Based Systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 67–82. Springer, Heidelberg (2008)

    Google Scholar 

  24. Habermehl, P., Iosif, R., Vojnar, T.: What Else Is Decidable about Integer Arrays? In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474–489. Springer, Heidelberg (2008)

    Google Scholar 

  25. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. (1994)

    Google Scholar 

  26. Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On Local Reasoning in Verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008)

    Google Scholar 

  27. Johnson, T.T., Mitra, S.: A Small Model Theorem for Rectangular Hybrid Automata Networks. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 18–34. Springer, Heidelberg (2012)

    Google Scholar 

  28. Legay, A., Bensalem, S., Boyer, B., Bozga, M.: Incremental generation of linear invariants for component-based systems. In: ACSD (2013)

    Google Scholar 

  29. Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: POPL (1997)

    Google Scholar 

  30. Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized networks of processes. Theor. Comput. Sci. 256(1–2) (2001)

    Google Scholar 

  31. Namjoshi, K.S.: Symmetry and Completeness in the Analysis of Parameterized Systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 299–313. Springer, Heidelberg (2007)

    Google Scholar 

  32. Pnueli, Amir, Ruah, Sitvanit, Zuck, Lenore D.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, Tiziana, Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)

    Google Scholar 

  33. Reich, J.: Processes, roles and their interactions. In: Proceedings of IWIGP (2012)

    Google Scholar 

  34. Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: AVMFSS (1989)

    Google Scholar 

  35. Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: FORTE (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Grenoble, Verimag, F-38000, Grenoble, France

    Lăcrămioara Aştefănoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga & Jacques Combaz

  2. CNRS, Verimag, F-38000, Grenoble, France

    Lăcrămioara Aştefănoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga & Jacques Combaz

Authors
  1. Lăcrămioara Aştefănoaei
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Souha Ben Rayana
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Saddek Bensalem
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Marius Bozga
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Jacques Combaz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lăcrămioara Aştefănoaei .

Editor information

Editors and Affiliations

  1. Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. Jet Propulsion Laboratory, Pasadena, California, USA

    Gerard Holzmann

  3. Jet Propulsion Laboratory, Pasadena, California, USA

    Rajeev Joshi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Aştefănoaei, L., Ben Rayana, S., Bensalem, S., Bozga, M., Combaz, J. (2015). Compositional Verification of Parameterised Timed Systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds) NASA Formal Methods. NFM 2015. Lecture Notes in Computer Science(), vol 9058. Springer, Cham. https://doi.org/10.1007/978-3-319-17524-9_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-17524-9_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-17523-2

  • Online ISBN: 978-3-319-17524-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation