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
- Java 1.6
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:
- First download the RVMT-BIP tool-set
- Extract the package. The main directory contains:
- lib/ directory that contains libraries used by the tool,
- bin/ directory that contains the tool binaries,
- setup.sh script to set up the environment, and
- README file that describes the tool in detail.
- 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),
$ source setup.sh
$ 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].
- 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:
$ ./system -s --threads [threads-number]