Abstract
We describe ASTRA (see http://rw4.cs.uni-saarland.de/~rtc/astra/), a tool for the static analysis of infinite-state graph transformation systems. It is based on abstract interpretation and implements cluster abstraction, i.e., it computes a finite overapproximation of the set of reachable graphs by decomposing them into small, overlapping clusters of nodes. While related tools lack support for negative application conditions, accept only a limited class of graph transformation systems, or suffer from state-space explosion on models with (even moderate) concurrency, ASTRA can cope with scenarios that combine these three challenges. Applications include parameterized verification and shape analysis of heap structures.
This work was partially supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS). See http://www.avacs.org/ for more information.
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
References
Backes, P.: dcs2gts - An interface between XML-coded DCS protocols and the hiralysis representation of graph transformation grammars. Fopra report, Saarland University, January 2007
Backes, P., Reineke, J.: Abstract topology analysis of the join phase of the merge protocol. In: TTC 2010, CTIT Workshop Proceedings, vol. WP10-03, pp. 127–133. University of Twente, Enschede (2010)
Backes, P., Reineke, J.: Analysis of infinite-state graph transformation systems by cluster abstraction. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 135–152. Springer, Heidelberg (2015)
Bauer, J., Schaefer, I., Toben, T., Westphal, B.: Specification and verification of dynamic communication systems. In: ACSD 2006, pp. 189–200 (2006)
Bauer, J.: Analysis of Communication Topologies by Partner Abstraction. Ph.D. thesis, Saarland University (2006)
Bauer, J., Toben, T., Westphal, B.: Mind the shapes: Abstraction refinement via topology invariants. Technical report 22, SFB/TR 14 AVACS, June 2007
König, B., Kozioura, V.: Augur 2–a new version of a tool for the analysis of graph transformation systems. In: Bruni, R., Varró, D. (eds.) GT-VMT 2006, ENTCS, vol. 2011, pp. 201–210 (2008)
Rakow, J.: Verification of Dynamic Communication Systems. Diploma thesis, Carl-von-Ossietzky Universität Oldenburg, April 2006
Zambon, E.: Abstract graph transformation : theory and practice. Ph.D. thesis, University of Twente (2013)
Acknowledgments
We thank Dmytro Puzhay for assistance with the implementation work and Jörg Bauer-Kreiker for providing his hiralysis test cases. Conny Clausen managed copyright clearance with Saarland University to obtain permission for releasing the tool under a Free Software license. Reinhard Wilhelm provided valuable comments for a draft version of this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Backes, P., Reineke, J. (2015). ASTRA: A Tool for Abstract Interpretation of Graph Transformation Systems. In: Fischer, B., Geldenhuys, J. (eds) Model Checking Software. SPIN 2015. Lecture Notes in Computer Science(), vol 9232. Springer, Cham. https://doi.org/10.1007/978-3-319-23404-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-23404-5_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23403-8
Online ISBN: 978-3-319-23404-5
eBook Packages: Computer ScienceComputer Science (R0)