Trace checking of Metric Temporal Logic with Aggregating Modalities using MapReduce
This work addresses the challenge of scalable trace checking for complex software systems, offering a domain-specific incremental improvement.
The paper tackles the problem of efficiently checking quantitative system requirements, expressed in a metric temporal logic with aggregating modalities, over large execution traces from logs, by presenting a MapReduce-based algorithm that achieves significant time gains and demonstrates scalability in implementation.
Modern complex software systems produce a large amount of execution data, often stored in logs. These logs can be analyzed using trace checking techniques to check whether the system complies with its requirements specifications. Often these specifications express quantitative properties of the system, which include timing constraints as well as higher-level constraints on the occurrences of significant events, expressed using aggregate operators. In this paper we present an algorithm that exploits the MapReduce programming model to check specifications expressed in a metric temporal logic with aggregating modalities, over large execution traces. The algorithm exploits the structure of the formula to parallelize the evaluation, with a significant gain in time. We report on the assessment of the implementation - based on the Hadoop framework - of the proposed algorithm and comment on its scalability.