Overview

DrAGoM (short for: Directed Abstract Graphs over Multiplicities) is a prototype tool to handle and manipulate multiply annotated type graphs which were originally introduced in this publication. The functionality of DrAGoM covers, among others, the computation of rewritable materializations and strongest postconditions in abstract graph rewriting.

The development of this tool is part of our research on the journey to find a suitable graph specification framework for verification purposes. The aim of this research is to provide verification techniques based on formal language theory and graph theory for graph transformation systems. The central notion is that of a multiply annotated type graph, which is an instance of an abstract graph, used to specify a (possibly infinite) graph language, i.e., a set of graphs.

The main application of DrAGoM is to automatically check invariants of graph transformation systems in the framework of abstract graph rewriting. For this purpose, given a graph language, the tool constructs an abstract graph which specifies the strongest postcondition wrt. a graph transformation system. To compute the strongest postcondition, DrAGoM uses a materialization construction to extract a concrete instance of the left-hand side out of the abstract graph in every possible way. Afterwards DrAGoM performs a language inclusion check to verify if the strongest postcondition is already covered by the initial graph language.

The theoretical framework on which this tool is based, is explained in this paper.

System requirements

DrAGoM is written in Java. It should run on any computer with a Java runtime environment installed (version 8 or newer); we recommend Oracle's JRE.

To compute annotations for the rewritable materialization, DrAGoM calls the external SMT solver Z3. For this functionality, you need to download a Z3 release which fits your operating system (available here). Please note that the folder which contains the libz3java dynamic link library (DLL) must be in the operating system's search path. Alternatively you can provide the path to the library file when launching the application (see the "Quick start" section below).

Please make sure that DrAGoM is allowed to create new files and directories (in the directory where you installed DrAGoM).

Usage

A detailed manual is available as PDF file in the download section.

Quick start

In most operating systems, double-clicking on the dragom.jar file will open DrAGoM in GUI-mode. Otherwise, the GUI can be directly started from the command-line as follows: Change to the directory where dragom.jar is located, and type:

java -jar dragom.jar

In some Linux operating systems, DrAGoM might not be able to immediately locate the folder containing the libz3java library. To help the tool find the required library please set the global variable named LD_LIBRARY_PATH to point to the corresponding folder path, i.e., launch DrAGoM by typing the following:

LD_LIBRARY_PATH=<PATH_TO_LIBRARY_FOLDER> java -jar dragom.jar

Using the GUI, the user can interactively create multiply annotated type graphs and graph transformation systems. Furthermore, these object can be used as input to the different algorithms to compute rewritable materializations, strongest postconditions or to perform an invariant check.

Input and output formats

For loading and storing multiply annotated type graphs, DrAGoM uses the XML based standard Graph eXchange Language (GXL). The DTD for the standard is given in the resource folder in the source code archive and can also be found on the GXL homepage.

Graph transformation systems are stored in a text-based format called Simple Graph File (SGF). A formal specification of the input format is given in Chapter 4 of this manual.