Abstract
We present a new abstraction technique for the exploration of graph transformation systems with infinite state spaces. This technique is based on patterns, simple graphs describing structures of interest that should be preserved by the abstraction. Patterns are collected into pattern graphs, layered graphs that capture the hierarchical composition of smaller patterns into larger ones. Pattern graphs are then abstracted to a finite universe of pattern shapes by collapsing equivalent patterns. This paper shows how the application of production rules can be lifted to pattern shapes, resulting in an over-approximation of the original system behaviour and thus enabling verification on the abstract level.
The work reported herein is being carried out as part of the GRAIL project, funded by NWO (Grant 612.000.632).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baldan, P., Corradini, A., König, B.: A Static Analysis Technique for Graph Transformation Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 381–395. Springer, Heidelberg (2001)
Bauer, J.: Analysis of Communication Topologies by Partner Abstraction. PhD thesis, Universität des Saarlandes (2006)
Bauer, J., Boneva, I., Kurban, M., Rensink, A.: A modal-logic based graph abstraction. In: [7]
Bauer, J., Wilhelm, R.: Static Analysis of Dynamic Communication Systems by Partner Abstraction. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 249–264. Springer, Heidelberg (2007)
Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic invariant verification for systems with dynamic structural adaptation. In: ICSE. ACM (2006)
de Lara, J., Varro, D. (eds.): GraBaTs. ECEASST, vol. 32. EASST (2010)
Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.): ICGT 2008. LNCS, vol. 5214. Springer, Heidelberg (2008)
Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using groove. STTT 14(1) (2012)
Ghamarian, A.H., Rensink, A., Jalali, A.: Incremental pattern matching in graph-based state space exploration. In: [6]
König, B., Kozioura, V.: Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 197–211. Springer, Heidelberg (2006)
König, B., Kozioura, V.: Augur 2 - a new version of a tool for the analysis of graph transformation systems. ENTCS 211 (2008)
Rensink, A.: The GROOVE Simulator: A Tool for State Space Generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004)
Rensink, A.: Canonical Graph Shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 401–415. Springer, Heidelberg (2004)
Rensink, A., Distefano, D.: Abstract graph transformation. In: Workshop on Software Verification and Validation (SVV). ENTCS, vol. 157 (2006)
Rensink, A., Zambon, E.: Neighbourhood abstraction in groove. In: [6]
Rensink, A., Zambon, E.: Pattern-based graph abstraction (extended version). Technical report, University of Twente, Enschede, The Netherlands (2012)
Rieger, S., Noll, T.: Abstracting complex data structures by hyperedge replacement. In: [7]
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ToPLaS 24(3) (2002)
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)
Zambon, E., Rensink, A.: Graph subsumption in abstract state space exploration. In: GRAPHITE (Pre-proceedings) (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rensink, A., Zambon, E. (2012). Pattern-Based Graph Abstraction. In: Ehrig, H., Engels, G., Kreowski, HJ., Rozenberg, G. (eds) Graph Transformations. ICGT 2012. Lecture Notes in Computer Science, vol 7562. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33654-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-33654-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33653-9
Online ISBN: 978-3-642-33654-6
eBook Packages: Computer ScienceComputer Science (R0)