Uncover

Uncover implements a backward search for graph transformation systems to solve the coverability problem.

This tool can be used to verify the correctness of a system (e.g. protocols, distributed systems, concurrent systems, etc.) modelled by graphs and graph transformation rules. Given a well-quasi-order, any error preserved by the order (i.e. if a graph contains the error, then any larger graph contains the error as well) can be represented by a finite set of minimal error graphs. This tool can check if an error graph is coverable by the graph transformation system and thus check if the error is reachable. The theoretical framework on which this tool is based, is explained in this paper. Currently, the subgraph and the minor ordering are implemented.

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

Uncover also has a GitHub page (created by Michael Emmi).

For 64-bit Linux systems a binary including the necessary libraries (see below) is available in the download section. On other systems Uncover may be compiled if the necessary libraries exist.

Compiling Uncover

Uncover is written in C++ using the C++11 standard. It currently compiles on Linux (tested on Ubuntu 14.04, Fedora 21) and Mac OS X with MacPorts (tested on Yosemite), but does not compile on Windows. Uncover uses the following external libraries:

• Boost (version 1.54)
  • more precisely: boost_system, boost_filesystem, boost_program_options, boost_regex and boost_unit_test_framework
• Xerces-C++ (version 3.1)

Note that for compilation the standard and development packages of the above libraries are necessary. The source code archive contains a CMake script (requiring CMake 2.8+) for generating the makefiles, which is capable of compiling with gcc and clang. The source code should be compilable with newer versions of the above libraries and may be compilable with older versions, but this was not tested.

Additional run requirements

The analysis procedures do not use other tools. However, Uncover provides scenarios to draw graphs and graph transformation systems. These scenarios only work if LaTeX and Graphviz (version 2.36) are installed and in the operating systems search path for binaries.

Currently, only the source code documentation exists. A more general description or manual will be published at a later time.

Running Uncover

Uncover is a command line tool and does not provide a graphical user interface. A detailed usage description can be printed via:

uncover -h

A list of all scenarios is available via "uncover -l" and the usage of a specific scenario s can be printed via "uncover -u s".

See the case studies archive for examples of using Uncover.

Input and output

For loading and storing graphs and graph transformation systems, Uncover uses the XML based standards GXL (for graphs) and GTXL (for transformation systems). DTDs for both standards are given in the resource folder in the source code archive. However, we modified the GTXL defintion to enable universally quantified rules. An adapted DTD (gtxl_mod.dtd) is also given in the resource folder.

uncover Binary for 64-Bit Linux systems; does not require Boost or Xerces to run

UncoverCaseStudies.tar.gz Archive containing some case studies (previously published and unpublished), including scripts for running them on Linux

UncoverDoc.tar.gz Archive containing the source code documentation

UncoverSources.tar.gz Archive containing the source code, including a resource folder and some build scripts

Uncover is developed and maintained by Jan Stückrath.

Uncover is currently in beta stage. If you find any bugs or other unexpected behavior, please send me an e-mail.

Of course, the software is provided "as-is", without any implied or expressed warranty of any kind. So don't sue me if it doesn't work as expected.