timescales is a benchmark generator for Metric Temporal Logic (MTL) monitoring tools. It is originally developed for the monitoring tool Reelay but distributed standalone. It generates an MTL specification (as a standard YAML file) and an input trace (as a standard CSV file) that satisfies the formula at every time point. For the benchmark generation, a set of predefined timed properties are available through the interface. Please see the help and documentation for more information.
The purpose of these benchmarks is to measure the performance and scalability of MTL monitoring tools with respect to large timing bounds in the specification over some typical cases. Ideally, the performance of real-time monitoring tools should remain constant when the base time unit has changed. This is due to that different (parts of) systems use different time scales up to orders of magnitude and the specification of slower systems contain large timing bounds.
The generator timescales includes a Makefile to demonstrate the generation of benchmarks. For each supported property, the command make small generates a benchmark that contains a specification with small timing bounds and a short trace. On the other hand, the command make large generates three benchmarks for each property with increasingly larger time bounds (1x, 10x, 100x) over traces with a length of 1 million. The large suite has a size of 400MB and is not included in the distribution. Finally the command make full extends the large suite by dense time behaviors. The large suite has a size of 550MB and is not included in the distribution. Besides these default benchkmark suites, the customization of benchmark generation can be done easily using the command line interface of timescales.
The full interface of the benchmark generator timescales is as follows:
usage: timescales [OPTIONS] PROPERTY
timescales is a benchmark generator for some pre-defined metric temporal logic properties
positional arguments:
property Supported properties are below:
absence_after_q UBOUND
absence_before_r UBOUND
absence_between_q_and_r LBOUND UBOUND
always_after_q UBOUND
always_before_r UBOUND
always_between_q_and_r LBOUND UBOUND
recurrence_globally UBOUND
recurrence_between_q_and_r UBOUND MIN_RECUR MAX_RECUR
response_globally LBOUND UBOUND
response_between_q_and_r LBOUND UBOUND MIN_RECUR MAX_RECUR
optional arguments:
-h, --help show this help message and exit
-d N, --duration N define the approximate duration for the trace
-l N, --lbound N define the lower bound for the property if available for the property
-u N, --ubound N define the upper bound for the property if available for the property
--persistent enable persistent trace generation
--min-recur N define the minimum number of recurrence in the trace if available for the property
--max-recur N define the maximum number of recurrence in the trace if available for the property
--name STRING define the name of specification (default: spec)
--condense N define the maximum amount of condensation in the generated trace (default: 0)
--failing-end disable appending a sequence to the trace to make the spec fail (default: false)
--future generate a future MTL formula (default: past)
--output-dir DIR use existing DIR as the directory to write output files in (default: current)
--format FORMAT select the output format in {csv, json, protobuf, flatbuf} (default: json)
The repository includes containerized benchmark environments for quick benchmarking for some runtime verification tools. Currently we support reelay, monpoly, aerial, and montre tools.
Reelay (https://github.com/doganulus/reelay)
git clone https://github.com/doganulus/timescales.git
cd timescales
make full
make benchmark-reelay
Monpoly (https://bitbucket.org/monpoly/monpoly)
git clone https://github.com/doganulus/timescales.git
cd timescales
make full
python scripts/to_monpoly.py
make benchmark-monpoly
Aerial (https://bitbucket.org/traytel/aerial)
git clone https://github.com/doganulus/timescales.git
cd timescales
make full
python scripts/to_monpoly.py
make benchmark-aerial
Montre (https://github.com/doganulus/montre)
git clone https://github.com/doganulus/timescales.git
cd timescales
make full
python scripts/to_montre.py
make benchmark-montre
Dogan Ulus. "Timescales: A Benchmark Generator for MTL Monitoring Tools". In: Proceedings of the Conference on Runtime Verification (RV). 2019.