Runtime Verification of Distributed Systems

RVDist is a prototype tool for LTL runtime verification of distributed (component-based) systems, written in the C++ programming language.

RVDist uses Spot platform which is a C++11 library for LTL manipulation, and BigInt library which allows us to do arithmetic on big size integers.

How To Run RVDist


  • C++11
  • Spot library
  • BigInt library

To run the RVDist tool, please follow these steps:

  1. First download the RVDist tool-set
  2. Extract the package.
  3. The main directory contains:
    1. Make directory that contains:
      • Main C++ codes and associated files,
      • A sample list of events,
      • A sample configuration file config.ini.
    2. examples/ directory that contains some examples in separate folders.
  4. To use the tool on command line, go to the Make directory and run the following commands:
    $ g++ -std=c++11 -lspot -lbigint -o main
    $ ./main

A virtual machine in which all the requirements are installed is available here. (Username: user, Password: z )