Graph Backwards Tool (GBT) project home page

News

  • November 2008
    • GBT source code available in svn repository. Please use this instead of previous binary distributions.
    • A number of SPIN and UPPAAL ad hoc routing protocol models are now available here.
  • September 2008
  • August 2008
    • GBT version 2.0 released.
      • This version includes support for abstraction using summary nodes.
  • May 2008

About the tool

GBT is a graph grammar verification tool written in C++, using the Standard Template Library (STL). For a description of the theory behind the tool, please see our TACAS'08 paper.

Input and output

The tool takes as input a file with extension .grm. This file has four sections. First is the initial: section where a .dot file with the initial system hypergraph is given. Next comes the rules: section where left and right hand sides of all the actions in the system model are given. These are also described as .dot files, separated by an arrow (->) to indicate which is the left and right hand side respectively; the left hand sides of actions are (abstract) patterns and the right hand sides are hypergraphs. (The node identifiers are used to determine the mapping between left and right hand sides of an action.) The two last sections are called bad: and invalid: and contain listings of .dot files with undesirable (abstract) patterns and type constraints respectively. An advantage of using the .dot format for describing hypergraphs and (abstract) patterns is that we can use existing tools, e.g., neato to generate images of the graphs for use in documentation and during development.

A language reference for .grm files is available here.

A verification session

When the tool starts, it parses the given .grm file and all the .dot files named in it. Then, the initial hypergraph, actions, impossible patterns and undesirable patterns are used as input to a symbolic backward reachability procedure. If this procedure terminates without reaching a set of configurations containing the initial graph, then verification successful is reported. Otherwise, an error trace, showing a sequence of actions leading to one of the undesirable graph patterns, is provided (if the -trace flag has been given to GBT). This enables the user to track, e.g., potential modeling errors efficiently.

Availability

GBT is available in source form under the GNU General Public License. Please see the SourceForge.net project site for information on how to access the source code. Graph grammar models we have verified using GBT are available here.

A number of ad hoc routing protocol models in other formalisms are also available here.

People

GBT is written by Oskar Wibling and Mayank Saksena. Please feel free to contact Oskar with questions, comments, etc.

Running GBT

To run GBT on a system model, go to the directory where the model is located (this is needed for GBT to find all the .dot files named in the .grm file).

GBT is started using the following command line string:

cat <.grm file> | <path to gbt>/gbt [-d] [-latex] [-trace] [-a] [-pclabel <PC>]

where

  • -d turns on debug mode (more verbose)
  • -latex generates latex source from the given system model (along with .dot files, from which .eps files can be generated. A makefile for building .ps and .pdf is available here.
  • -trace outputs error trace(s), in case verification fails
  • -a enables abstraction using summary nodes (also enables -trace)
  • -pclabel <PC> enables zero-arity edges with labels starting "PC" to be interpreted as a certain program line, i.e., "PC2" in a hypergraph or abstract pattern will mean "program is at line 2".

For example, assume that we are positioned in the folder reverse_gbt, where the PALE reverse model is located. The GBT binary (called gbt) is located in the folder above. The command line string used to run a verification session, with error trace functionality turned on, is then:

cat reverse_auto_verification.grm | ../gbt -a -pclabel PC -trace

Verified graph grammar models

See this page for a list of example graph grammar models.

References

[1] Barbara König and Vitali Kozioura. Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In Proc. TACAS'06, 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pages 197-211, Springer, 2006.

[2] PALE - the Pointer Assertion Logic Engine examples.

[3] Mayank Saksena, Oskar Wibling, and Bengt Jonsson. Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols. Proc. TACAS'08, 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2008. [PDF] [Presentation] [Extended version]

Internal TODO list

Our TODO list can be found here (only for internal use; requires logging in).