A tool for abstract analysis of graph transformation systems
*This work is supported by the DFG as part of the Transregional Collaborative Research Center SFB/TR 14 AVACS.
ASTRA computes abstract graph transformations. It takes a human readable specification of a graph transformation system as input. This specification describes the generation of graphs of infinite size; ie., graphs with an infinite number of nodes and edges. The graph transformation system consists of a set of single pushout graph transformation rules, each of which replaces a subgraph by another subgraph. The subgraph to be replaced can be annotated with local negative application conditions ("partner constraints"). ASTRA uses a finite representation to over-approximate the infiniteness in the resulting graphs. The rule transformations of the system will applied on this abstract representation.
The most common practical use for ASTRA is the static analysis and verification of topology structures of dynamic communication systems, ie., systems where the number of participants is not bounded in advance. However, the concepts are not limited to some specific purpose. The tool can, in principle, be used for anything that can reasonably be represented in the formalism. To a certain degree, shape analysis of heap structures can be done, for example.
ASTRA reads graph tranformation systems in the same file format that is used by hiralysis. (hiralysis is a tool written by Joerg Bauer-Kreiker for the same purpose but using a different abstraction technique, partner abstraction.) The output can be written in a number of file formats:
- DOT (Graphviz)
- GML (OGDF resp. GoVisual Diagram Editor)
- GDL (VCG resp. aiSee)
- GraphML (yEd resp. yComp)
- mp (MetaPost)
- GTS (native file format)
- XGDL (native XML based file format)
Interesting part of merge protocol with serial leader notification, layouted with yed