Overview

The aim of this project is to provide verification techniques based on formal language theory and graph theory for graph transformation systems. The central notion of this project is that of a graph automaton, which is a generalization of finite automata to process graphs instead of words.

Raven is a tool suite to handle and manipulate graph automata up to a bounded interface size (respectively up to a bounded pathwidth). The functionality of Raven covers among others the computation of pre-defined classes of automata (k-colorability automaton, subgraph isomorphism automaton, vertex cover automaton, ...), which can be combined by computing union or product automata, thus realising closure properties, and to check the membership of a given graph in the language defined by an automaton.

One of the main applications of Raven is to automatically check invariants of graph transformation systems. Another feature of Raven is the possibility to solve the language inclusion problem for two given graph automata which is implemented via recent algorithms for finite automata. Furthermore, Raven also offers algorithms to perform both emptiness and universality checks.

The development of this tool is part of the GaReV project (related Publications).

System requirements

Raven is written in Java. It should run on any computer with a Java runtime environment installed (version 7 or newer); we recommend Oracle's JRE. Furthermore, the program GraphViz (available at www.graphviz.org) is needed to draw graphs in the graphical user interface. Beside that no further installation is necessary to run Raven. All other libraries are directly included in the zip-file.

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

Usage

For a detailed manual see the documentation, which is available as PDF file in the download section.

Quick start

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

java -jar raven.jar

Using the GUI, the user can interactively create graph automata, graphs and cospans of graphs. Furthermore, these object can be used as input to the different algorithms to check the membership, emptiness, universality, language inclusion or invariant problem.

To run the program from the command line, change to the directory where raven.jar is located, and type:

java -jar raven.jar -c [scriptFile]

where scriptFile indicates a script file in the script directory.