THEMIS - A Tool for Decentralized Monitoring Algorithms

The artifact repository for the ISSTA 2017 paper: Monitoring Decentralized Specifications.

Reading the README.md Files

All README.md files are pre-rendered as HTML for convenience. In each directory (including this one), the index.html file corresponds to a rendered README.md.

Related Papers

• Antoine El-Hokayem and Ylies Falcone. 2017. Monitoring Decentralized Specifications. In Proceedings of the 26th International Symposium on Softare Testing and Analysis, ISSTA 2017, Santa-Barbara, USA, July 10-14, 2017. To appear.

Exploring the Artifacts

Using the Docker Container

An environment for exploring the artifacts is provided as a docker container with all needed dependencies. We provide the Dockerfile to build the image. For more instructions see the docker folder and the docker/README.md file.

Setup without Docker

If you wish to run the tool without docker.

• Install AspectJ or extract it from aspectj.tgz.
• Download and extract all third-party dependencies in third.tgz.
• Configure the environment variables (add all exports from .bashrc to your .bashrc or startup shell).

Dependencies:

• Spot (Particularly: ltlfilt) for minimizing LTL and boolean formulae.
• LTL3Tools for converting LTL formulae into monitor automata.
• AspectJ for compiling measures (not running).

We note that we use a patched ltl2mon script that reads the formula from STDIN instead of arguments. This is due to the limit on the size of passing arguments. The patched script is found in third/ltl3tools-0.0.7/ltl2mon.

Artifacts

The THEMIS artifacts are presented each in a folder, check the sub-folder README.md files for instructions on exploring and reproducing the artifacts.

The artifacts are as follows:

• data.dat (plot) : the data used for the table in the paper;
• run.db (experiments) : an SQLite file with the raw data of all experiments;
• themis.jar (source) : the THEMIS software;
• example.jar (example) : an example monitoring algorithm and measure designed to illustrate THEMIS integration.

We provide both the artifacts and the necessary steps to re-create them.

Below is a list of artifacts along with their dependencies, their files, and the time needed to reproduce them.

plot

The plot folder contains our processing of the data (normalization, aggregation), plots, and tables generation.

• Depends on: run.db (experiments)
• Generates: data.dat, graphs, tables
• Time: ~ 5-10 minutes

experiments

The experiments folder contains our experimental setup. This includes the raw data and ability to re-run the experiments.

• Depends on: themis.jar (source)
• Generates: run.db
• Time: ~ 24-30 hours

source

The source folder provides the THEMIS framework tool along with its source code, and instructions to build and run the tools.

• Depends on: none
• Generates: themis.jar
• Time: ~ 5-15 minutes

example

The example folder contains an example measure and algorithms to integrate with THEMIS. It is used to showcase how it is possible to design new algorithms and measures with THEMIS. An example test experiment is provided.

• Depends on: themis.jar (source)
• Generates: example.jar
• Time: ~ 1-2 minutes