Skip to main content
SpringerLink
Log in

Symmetry for the Analysis of Dynamic Systems

  • Conference paper
NASA Formal Methods (NFM 2011)

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

Included in the following conference series:

Abstract

Graph Transformation Systems (GTSs) provide visual and explicit semantics for dynamically evolving multi-process systems such as network programs and communication protocols. Existing symmetry reduction techniques that generate a reduced, bisimilar model for alleviating state explosion in model checking are not applicable to dynamic models such as those given by GTSs. We develop symmetry reduction techniques applicable to evolving GTS models and the programs that generate them. We also provide an on-the-fly algorithm for generating a symmetry-reduced quotient model directly from a set of graph transformation rules. The generated quotient model is GTS-bisimilar to the model under verification and may be exponentially smaller than that model. Thus, analysis of the system model can be performed by checking the smaller GTS-bisimilar model.

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. Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters 22, 307–309 (1986)

    Article  Google Scholar 

  2. Baldan, P., Corradini, A., König, B.: Verifying finite-state graph grammars: an unfolding-based approach. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 83–98. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Baresi, L., Heckel, R.: Tutorial introduction to graph transformation: A software engineering perspective. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 402–429. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic counter abstraction for concurrent software. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 64–78. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic invariant verification for systems with dynamic structural adaptation. In: ICSE 2006, pp. 72–81 (2006)

    Google Scholar 

  6. Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  7. Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods in Sys. Des. 9(1-2), 77–104 (1996)

    Article  Google Scholar 

  8. Degano, P., Montanari, U.: A model for distributed systems based on graph rewriting. J. ACM 34(2), 411–449 (1987)

    Article  Google Scholar 

  9. Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Methods Syst. Des. 9(1/2), 105–131 (1996)

    Article  Google Scholar 

  10. Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  11. Heckel, R.: Compositional verification of reactive systems specified by graph transformation. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, p. 138. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. Iosif, R.: Symmetry reduction criteria for software model checking. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 22–41. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Ip, C.N., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1-2), 41–75 (1996)

    Article  Google Scholar 

  14. Langari, Z.: Modelling and Analysis using Graph Transformation Systems. Ph.D. thesis, University of Waterloo, Waterloo, Canada (2010)

    Google Scholar 

  15. Langari, Z., Trefler, R.: Formal modeling of communication protocols by graph transformation. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol. 4085, pp. 348–363. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Langari, Z., Trefler, R.: Application of graph transformation in verification of dynamic systems. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 261–276. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. McKay, B.: Practical graph isomorphism. Congressus Numerantium 30, 45–87 (1981)

    MATH  Google Scholar 

  18. Rensink, A.: Isomorphism checking in groove. ECEASST 1 (2006)

    Google Scholar 

  19. Rensink, A.: Explicit state model checking for graph grammars. In: Degano, P., De Nicola, R., Bevilacqua, V. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 114–132. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  20. Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformations. Foundations, vol. 1. World Scientific, Singapore (1997)

    MATH  Google Scholar 

  21. Trefler, R.J., Wahl, T.: Extending symmetry reduction by exploiting system architecture. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 320–334. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. David R. Cheriton School of Computer Science, University of Waterloo, ON, Canada

    Zarrin Langari & Richard Trefler

Authors
  1. Zarrin Langari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Richard Trefler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA Jet Propulsion Laboratory, 4800 Oak Grove Drive, M/S 301-285, 91109, Pasadena, CA, USA

    Mihaela Bobaru , Klaus Havelund , Gerard J. Holzmann  & Rajeev Joshi , ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Langari, Z., Trefler, R. (2011). Symmetry for the Analysis of Dynamic Systems. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-20398-5_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-20397-8

  • Online ISBN: 978-3-642-20398-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation