Skip to main content
SpringerLink
Log in

Uncover: Using Coverability Analysis for Verifying Graph Transformation Systems

  • Conference paper
  • First Online:
Graph Transformation (ICGT 2015)

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

Included in the following conference series:

Abstract

Uncover is a tool for high level verification of distributed or concurrent systems. It uses graphs and graph transformation rules to model these systems in a natural way. Errors in such a system are modelled by upward-closed sets for which two orders are provided, the subgraph and the minor ordering. We can then exploit the theory of well-structured transition systems to obtain exact or approximating decidability results (depending on the order and system) for the question whether an error can occur or not. For this framework we also introduced an extension of classical graph transformation which is capable of modelling broadcast protocols.

Research partially funded by DFG project GaReV.

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

Institutional subscriptions

Notes

  1. 1.

    G is an induced subgraph of \(G'\) if we can obtain G by deleting a subset of the nodes of \(G'\) including their incident edges.

References

  1. Abdulla, P.A., Bouajjani, A., Cederberg, J., Haziza, F., Rezine, A.: Monotonic abstraction for programs with dynamic memory heaps. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 341–354. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Abdulla, P.A., C̆erāns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS 1996, pp. 313–321. IEEE (1996)

    Google Scholar 

  3. AUGUR2. http://www.ti.inf.uni-due.de/research/tools/augur2/

  4. Bansal, K., Koskinen, E., Wies, T., Zufferey, D.: Structural counter abstraction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 62–77. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  5. Bertrand, N., Delzanno, G., König, B., Sangnier, A., Stückrath, J.: On the decidability status of reachability and coverability in graph transformation systems. In: Proceedings of RTA 2012, vol. 15 of LIPIcs, pp. 101–116 (2012)

    Google Scholar 

  6. Delzanno, G., Stückrath, J.: Parameterized verification of graph transformation systems with whole neighbourhood operations. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 72–84. Springer, Heidelberg (2014)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  8. Graph Backwards Tool (GB). http://www.it.uu.se/research/group/mobility/adhoc/gbt

  9. Graphviz website. http://www.graphviz.org/

  10. GROOVE. http://groove.cs.utwente.nl/

  11. Holt, R.C., Schürr, A., Sim, S.E., Winter, A.: GXL. http://www.gupro.de/GXL/

  12. Joshi, S., König, B.: Applying the graph minor theorem to the verification of graph transformation systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 214–226. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  13. König, B., Stückrath, J.: Well-structured graph transformation systems with negative application conditions. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 81–95. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  14. König, B., Stückrath, J.: A general framework for well-structured graph transformation systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 467–481. Springer, Heidelberg (2014)

    Google Scholar 

  15. Meyer, R.: Structural stationarity in the \(\pi \)-calculus. Ph.D. thesis, Carl-von-Ossietzky-Universität Oldenburg (2009)

    Google Scholar 

  16. Robertson, N., Seymour, P.: Graph minors XXIII. Nash-Williams’ immersion conjecture. J. Comb. Theory, Ser. B 100, 181–205 (2010)

    Article  MathSciNet  Google Scholar 

  17. Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation: Volume 1: Foundations. World Scientific Publishing, River Edge (1997)

    Google Scholar 

  18. Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 18–32. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. Stückrath, J.: UNCOVER. http://www.ti.inf.uni-due.de/research/tools/uncover/

Download references

Author information

Authors and Affiliations

  1. Universität Duisburg-Essen, Essen, Germany

    Jan Stückrath

Authors
  1. Jan Stückrath
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jan Stückrath .

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Sapienza Università di Roma, Rome, Italy

    Francesco Parisi-Presicce

  2. Angewandte Informatik 1, Universität Bayreuth, Bayreuth, Germany

    Bernhard Westfechtel

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Stückrath, J. (2015). Uncover: Using Coverability Analysis for Verifying Graph Transformation Systems. In: Parisi-Presicce, F., Westfechtel, B. (eds) Graph Transformation. ICGT 2015. Lecture Notes in Computer Science(), vol 9151. Springer, Cham. https://doi.org/10.1007/978-3-319-21145-9_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-21145-9_17

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation