Timescales: A Benchmark Generator for MTL Monitoring Tools

This article presents a benchmark generator, Timescales, which can be used to evaluate the performance and scalability of runtime verification tools using Metric Temporal Logic (MTL) formulas as their specifications. We mainly target runtime verification of cyber-physical systems and generate traces similar to the qualitative behavior of sensor readings and state variables of such systems that are observed/sampled continuously. Since such systems are composed of many heterogeneous components that work over very different time scales, it is crucial to measure the performance of the MTL monitoring tool for a wide range of timing parameters in specifications. Hence, Timescales supports the generation of benchmarks for 10 typical timed properties for any given trace length and timing parameters with several other useful features. Finally, we include some default benchmark suites generated by Timescales.