Runtime Verification of Multi-Threaded BIP

RVMT-BIP is a Runtime Verification tool integrated in the BIP tool suite. BIP (Behavior, Interaction, Priority) is a powerful and expressive component-based framework for the formal construction of heterogeneous systems. It is developed at Verimag Laboratory. [more about BIP]

RVMT-BIP takes as input a BIP model and an abstract description of a monitor (an XML file), and outputs a new BIP system whose behavior is monitored while running with a multi-threaded centralized controller.

How To Install and Run RVMT-BIP

Requirements:

  • Linux.
  • Java 1.6
  • C++11

We note that RVMT-BIP takes as input a BIP system modeled following the new BIP language. To install the RVMT-BIP tool, please follow these steps:

  1. First download the RVMT-BIP tool-set
  2. Extract the package.
  3. The main directory contains:
    1. lib/ directory that contains libraries used by the tool,
    2. bin/ directory that contains the tool binaries,
    3. setup.sh script to set up the environment, and
    4. README file that describes the tool in detail.
    5. examples/ directory that contains some examples in separate folders, each folder contains:
      • A BIP file,
      • External C++ codes (if applicable),
      • source/ directory that contains the properties to ckeck,
        • Monitor.xml monitor given as input,
        • Map_Event_Guard map each event in the monitor to a guard on the variable/states/ports of atomic components,
        • Guide list of variables and components to monitor (used in Map_Event_Guard),
  4. To use the tool on command line, you have to source the setup.sh in order to add the binary files to you path:
    $ source setup.sh
  5. Go to the RVMT main directory and make sure that bin/RVMT is executable (chmod u+x bin/RVMT), then choose a specific example directory in examples/ and run the RVMT-BIP tool to build monitored version of your selected example model, using this command:
    $ RVMT [name-of-input-package] [name-of-root-component] [path-to-output-file]
    • RVMT takes an input BIP model, which is specified by package name and root-component name. The package name is matched the file name that contains it (ie. package Sample is stored in a file named Sample.bip) and root-component name is the declaration of compound type.
    • The output results, which are the monitored version of input model along with two other files (RGT.cpp and RGT.hpp) as further execution requirements, will be stored in [path-to-output-file].
  6. Code generation, compile and execute the monitored BIP file. Note that, for this step it is prerequisite that the BIP engine is already installed on your machine. [more info]
    • code generation:
      $ bipc.sh -I . -p [input-monitored-model] -d [name-of-root-component] --gencpp-output-dir [path-to-output-file] --gencpp-follow-used-packages --gencpp-ld-l pthread --gencpp-cc-I $PWD
      $ cmake ..
    • compile and execute:
      $ make
      $ ./system -s --threads [threads-number]

Examples

  • System Task

  • Reader-Writer

  • Dining Philosophers

  • Demo